let V be finite-dimensional RealLinearSpace; :: thesis: dim V = dim ((Omega). V)

consider I being finite Subset of V such that

A1: I is Basis of V by Def1;

A2: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def 4

.= Lin I by A1, RLVECT_3:def 3 ;

( card I = dim V & I is linearly-independent ) by A1, Def2, RLVECT_3:def 3;

hence dim V = dim ((Omega). V) by A2, Th29; :: thesis: verum

consider I being finite Subset of V such that

A1: I is Basis of V by Def1;

A2: (Omega). V = RLSStruct(# the carrier of V, the ZeroF of V, the U5 of V, the Mult of V #) by RLSUB_1:def 4

.= Lin I by A1, RLVECT_3:def 3 ;

( card I = dim V & I is linearly-independent ) by A1, Def2, RLVECT_3:def 3;

hence dim V = dim ((Omega). V) by A2, Th29; :: thesis: verum