Every nonzero unitary representation of a compact group has a finite-dimensional subrepresentation

Fix $v\in H$ with $v\mathrm{\ne }0$; by [F1] there is $f\in C(K)$ with $\pi (f)v\mathrm{\ne }0$. Since $\mu (K)=1$ the uniform norm dominates the $L^1$ norm, so uniform density [F2] provides $f_1\in R(K)$ with $\mathrm{\parallel }f-f_1{\mathrm{\parallel }}_{\mathrm{\infty }}<\mathrm{\parallel }\pi (f)v\mathrm{\parallel }\mathrm{/}(2\mathrm{\parallel }v\mathrm{\parallel })$ and hence $\mathrm{\parallel }\pi (f-f_1)v\mathrm{\parallel }\le \mathrm{\parallel }f-f_1{\mathrm{\parallel }}_1\mathrm{\parallel }v\mathrm{\parallel }\le \mathrm{\parallel }f-f_1{\mathrm{\parallel }}_{\mathrm{\infty }}\mathrm{\parallel }v\mathrm{\parallel }<\mathrm{\parallel }\pi (f)v\mathrm{\parallel }\mathrm{/}2$; therefore $\mathrm{\parallel }\pi (f_1)v\mathrm{\parallel }\ge \mathrm{\parallel }\pi (f)v\mathrm{\parallel }-\mathrm{\parallel }\pi (f-f_1)v\mathrm{\parallel }>0$, that is $\pi (f_1)v\mathrm{\ne }0$.

Write $f_1$ as a finite linear combination of matrix coefficients of finite-dimensional continuous unitary representations ${\pi }_1,\dots ,{\pi }_r$ of $K$, and let $E\subseteq C(K)$ be the linear span of all matrix coefficients of these representations; then $E$ is finite dimensional because each ${\pi }_j$ has only $d_j^2$ coefficients in an orthonormal basis, and $E$ is invariant under left translation by [F3]; the set $F:=\{\pi (h)v:h\in E\}$ is the image of the finite-dimensional space $E$ under the linear map $h\mapsto \pi (h)v$, so it is a finite-dimensional linear subspace of $H$ containing $\pi (f_1)v\mathrm{\ne }0$. For $k\in K$ and $h\in E$ the covariance [F4] gives $\pi (k)(\pi (h)v)=\pi (\lambda (k)h)v\in F$, so $\pi (k)F\subseteq F$; replacing $k$ by $k^{-1}$ gives $F\subseteq \pi (k)F$, hence $\pi (k)F=F$ for every $k$, and $F$ is closed by [F5] because it is finite dimensional. Thus $F$ is a nonzero finite-dimensional closed $\pi (K)$-invariant subspace of $H$, which proves the lemma. The Axiom of Choice is inherited through the $L^1$ action and the uniform-density supplier; the finite-dimensional-span argument is choice-free apart from those inputs.