Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$. Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\, c_F(H_1,...,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,...,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristics of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite of this, the function $f_n$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.

I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$. I argue as follows. Consider arbitrary element $a\in A_{n}(c)$. Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that $\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$. Thus $a\leqslant g_n(c)$. Since this inequality holds for every $a\in A_{n}(c)$, we conclude that $\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because we need to choose an element (system of subspaces) from a class (and work with this element). Do we need here something like the Axiom of Choise?

In response to Nate Eldredge's comment: essentially, the core of my worries is the following. Unfortunately, and this is the worst, is that I do not understand if the function $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$, is needed in the arguments above or not.

Please help me.

Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$. Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\, c_F(H_1,...,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,...,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristics of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite of this, the function $f_n$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.

I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$. I argue as follows. Consider arbitrary element $a\in A_{n}(c)$. Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that $\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$. Thus $a\leqslant g_n(c)$. Since this inequality holds for every $a\in A_{n}(c)$, we conclude that $\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because we need to choose an element (system of subspaces) from a class (and work with this element). Do we need here something like the Axiom of Choice?

In response to Nate Eldredge's comment: essentially, the core of my worries is the following. Unfortunately, and this is the worst, is that I do not understand if the function $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$, is needed in the arguments above or not.

Please help me.

Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$. Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\, c_F(H_1,...,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,...,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristics of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite of this, the function $f_n$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.

I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$. I argue as follows. Consider arbitrary element $a\in A_{n}(c)$. Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that $\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$. Thus $a\leqslant g_n(c)$. Since this inequality holds for every $a\in A_{n}(c)$, we conclude that $\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because we need to choose an element (system of subspaces) from a class (and work with this element). Do we need here something like the Axiom of Choise?

Let $H$ be a complex Hilbert space and $H_1,...,H_n$ be closed subspaces of $H$. Set $H_0:=H_1\cap H_2\cap...\cap H_n$ and let $P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,...,n$. I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by $$ f_n(c)=\sup\{\|P_n...P_2 P_1-P_0\|\,|\, c_F(H_1,...,H_n)\leqslant c\},\,c\in[0,1], $$ where the supremum is taken over all complex Hilbert spaces $H$ and systems of closed subspaces $H_1,...,H_n$ of $H$ for which the Friedrichs number $c_F(H_1,...,H_n)$ is less than or equal to $c$ (the Friedrichs number is a certain numerical characteristics of a system of subspaces). Note that all such systems of subspaces do not form a set. Despite of this, the function $f_n$ is well-defined (see my Question Can we take a supremum over all Hilbert spaces?). Indeed, let $A_{n}(c)$ be the set of all $a\in\mathbb{R}$ for which there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. Then by the axiom (scheme) of separation $A_{n}(c)$ is a set and thus we can take its supremum.

I need to show that $f_n(c)\leqslant g_n(c)$ for some function $g_n$. I argue as follows. Consider arbitrary element $a\in A_{n}(c)$. Then there exist a complex Hilbert space $H$ and a system of closed subspaces $H_1,...,H_n$ of $H$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$. After this I work with this system of subspaces $(H;H_1,...,H_n)$ and show that $\|P_n...P_2 P_1-P_0\|\leqslant g_n(c)$. Thus $a\leqslant g_n(c)$. Since this inequality holds for every $a\in A_{n}(c)$, we conclude that $\sup A_{n}(c)\leqslant g_n(c)$, i.e., $f_n(c)\leqslant g_n(c)$.

Questions. Are all these arguments correct, say, in the axiomatic theory ZFC? I am suspicious here because we need to choose an element (system of subspaces) from a class (and work with this element). Do we need here something like the Axiom of Choise?

In response to Nate Eldredge's comment: essentially, the core of my worries is the following. Unfortunately, and this is the worst, is that I do not understand if the function $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$ such that $c_F(H_1,...,H_n)\leqslant c$ and $\|P_n...P_2 P_1-P_0\|=a$, is needed in the arguments above or not.

Please help me.