For an orthonormal basis , define the Hilbert-Schmidt norm by . For a possibly uncountable basis, the nonnegative sum means the supremum over finite subsets. Parseval's identity gives, for any other orthonormal basis ,
Changing the domain basis in the last expression proves basis independence. Polarization gives a basis-independent inner product
with the same first-argument linear convention. The sums converge by the Cauchy-Schwarz inequality. The operator-norm bound follows by applying Cauchy-Schwarz to the coordinates of a unit vector.
To prove completeness, let be Cauchy in this norm. The operator-norm bound gives a bounded-operator limit . For a finite subset of the basis,
For large , the right side is uniformly small by the Cauchy property. Taking the supremum over shows is Hilbert-Schmidt and ; it also shows is Hilbert-Schmidt. Thus the Hilbert-Schmidt operators form a Hilbert space. Finite-rank operators are dense there: keeping finitely many basis columns makes the sum of omitted squared column norms tend to zero. The operator-norm bound then shows that every Hilbert-Schmidt operator is compact.
Now let be a strongly continuous unitary representation of the compact metric group , as is standard for a representation of a topological group. Fix and average the positive rank-one operator :
The integrand is continuous in the Hilbert-Schmidt norm, so this Bochner integral exists in the complete space just proved. Normalized Haar measure and invariance show that is positive, compact and commutes with every . Moreover,
the integrand is positive near the identity and every nonempty open set has positive Haar measure. Thus . A nonzero eigenspace is finite-dimensional and invariant under , by (a). Within it choose a nonzero invariant subspace of smallest dimension; it is irreducible. Its orthogonal complement is invariant because the representation is unitary, so the finite-dimensional space splits into irreducibles.
Take a maximal orthogonal family of such finite-dimensional irreducible invariant subspaces. If their closed span had a nonzero orthogonal complement, the same averaging argument on that complement would produce another member, contradicting maximality. Therefore
This compact averaging of a rank-one operator argument does not require itself to be separable. Strong continuity is the topological representation hypothesis used in the averaging step.