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 1;
A2: (Omega). V = ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) by VECTSP_4:def 4
.= Lin I by A1, VECTSP_7:def 3 ;
( card I = dim V & I is linearly-independent ) by A1, Def1, VECTSP_7:def 3;
hence dim V = dim ((Omega). V) by A2, Th26; :: thesis: verum