let V be finite-dimensional RealUnitarySpace; :: thesis: dim V = dim ((Omega). V)
consider I being finite Subset of V such that
A1: I is Basis of V by Def1;
A2: card I = dim V by A1, Def3;
A3: I is linearly-independent by A1, RUSUB_3:def 2;
(Omega). V = UNITSTR(# the carrier of V,the U2 of V,the addF of V,the Mult of V,the scalar of V #) by RUSUB_1:def 3
.= Lin I by A1, RUSUB_3:def 2 ;
hence dim V = dim ((Omega). V) by A2, A3, Th9; :: thesis: verum