Nonzero finite dimensional complex invariant subspaces have unitary eigenvectors

Invariance makes $U{\mathrm{\mid }}_E:E\to E$ a complex-linear endomorphism. The field $\mathbb{C}$ satisfies the algebraic-closedness hypothesis of F2 by F3. Since $\dim E\ge 1$, F2 yields $\lambda \in \mathbb{C}$ and a nonzero $f\in E$ with $Uf=\lambda f$. This uses a single finite-dimensional eigenvalue assertion; it selects no infinite family of eigenvectors.

Isometry gives $\mathrm{\parallel }f\mathrm{\parallel }=\mathrm{\parallel }Uf\mathrm{\parallel }=\mathrm{\mid }\lambda \mathrm{\mid }\mathrm{\parallel }f\mathrm{\parallel }$. Since $f\mathrm{\ne }0$, positivity permits division by $\mathrm{\parallel }f\mathrm{\parallel }$, giving $\mathrm{\mid }\lambda \mathrm{\mid }=1$. If also $E\subseteq H_0$ and $f=c\mathbf{1}$, then $0=\int f=c$ because the total measure is one. This would give $f=0$, impossible. Thus in that case $f$ is nonconstant. The case $\dim E=1$ is included; $E=\{0\}$ is excluded before F2 is applied.