let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF holds dim V = dim ((Omega). V)
let V be finite-dimensional VectSp of GF; :: thesis: dim V = dim ((Omega). V)
consider I being finite Subset of V such that
A1: I is Basis of V by MATRLIN:def 3;
A2: card I = dim V by A1, Def2;
A3: I is linearly-independent by A1, VECTSP_7:def 3;
(Omega). V = VectSpStr(# the carrier of V,the U5 of V,the U2 of V,the lmult of V #) by VECTSP_4:def 4
.= Lin I by A1, VECTSP_7:def 3 ;
hence dim V = dim ((Omega). V) by A2, A3, Th30; :: thesis: verum