This question is related to my question Can we choose an element from a class?. However, I decided to create a separate question.

Let $H$ be a complex Hilbert space and $H_1,\dotsc,H_n$ be closed subspaces of $H$.
Set $H_0\mathrel{:=}H_1\cap H_2\cap\dotsb\cap H_n$ and let
$P_i$ be the orthogonal projection onto $H_i$, $i=0,1,2,\dotsc,n$.
I study the functions $f_n:[0,1]\to\mathbb{R}$ defined by
$$
f_n(c)=\sup\{\lVert P_n\dotsm P_2 P_1-P_0\rVert \mathrel|
c_F(H_1,\dotsc,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,\dotsc,H_n$ of $H$
for which the Friedrichs number $c_F(H_1,\dotsc,H_n)$ is less than or equal to $c$
(the Friedrichs number is a certain numerical characteristic of a system of subspaces).
Note that all such systems of subspaces **do not** form a set.
Despite 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,\dotsc,H_n$ of $H$ such that
$c_F(H_1,\dotsc,H_n)\leqslant c$ and $\lVert P_n\dotsm P_2 P_1-P_0\rVert=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,\dotsc,H_n$ of $H$ such that $c_F(H_1,\dotsc,H_n)\leqslant c$ and $\lVert P_n\dotsm P_2 P_1-P_0\rVert=a$. After this I work with this system of subspaces $(H;H_1,\dotsc,H_n)$ and show that $\|P_n\dotsm 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?
Essentially, the core of my worries is the following.
Unfortunately, I do not understand if the **function** $A_n(c)\ni a\mapsto (H;H_1,...,H_n)$
such that $c_F(H_1,\dotsc,H_n)\leqslant c$ and $\lVert P_n\dotsm P_2 P_1-P_0\rVert=a$,
is needed in the arguments above or not.
If a function is needed here, it turns out that the "Axiom of Choice for classes" is needed here,
and I do not know what to do with this.
On the one hand, it seems that the function is not needed here.
On the other hand, we choose a system of subspaces for each $a\in A_n(c)$;
the set $A_n(c)$ can be infinite and we need to consider **all** $a\in A_n(c)$.
Therefore, perhaps, a function is needed here.
**Explain to me, please, whether a function is needed here or not?**

Please help me.

oneelement from a non-empty class; that's what non-empty means. You only need AC to makemanychoices simultaneously. See, for example, mathoverflow.net/questions/387353/… . $\endgroup$ – LSpice Apr 7 at 21:47`\dots`

commands are for. Compare the spacing in $H_1 \cap H_2 \cap \dotsb \cap H_n$`H_1 \cap H_2 \cap \dotsb \cap H_n`

to that in $H_1 \cap H_2 \cap ... \cap H_n$`H_1 \cap H_2 \cap ... \cap H_n`

. I have edited accordingly. $\endgroup$ – LSpice Apr 7 at 21:53