I think its more productive to view these as elements of
Proof of orthonormality
Let be an arbitrary linear map.
Define a linear map
It follows that for any
so is an intertwining operator
and therefore by Schur’s lemma either or ,
so with .
Combining these two possibilities gives
If we chose to then , thus
thus the matrix elements fulfil the orthonormality condition.
Proof of spanning set
Let , so we must prove .
The tensor product of irreps is reducible, which for concrete reälizations may be stated as
for some numbers .
Thus the point-wise product of basic functions is in ,
and by distributivity is closed under point-wise multiplication.
Since Irreps collectively distinguish group elements,
it follows from Finite version that .
From this and above, is an orthonormal basis under .
Since the number of basis elements equals the dimension of the vector space, it follows that Square sum of irrep dimensions is given by