let V be finite-dimensional RealLinearSpace; :: thesis: for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let W be Subspace of V; :: thesis: ( dim V = dim W iff (Omega). V = (Omega). W )

hereby :: thesis: ( (Omega). V = (Omega). W implies dim V = dim W )

assume A1: dim V = dim W ; :: thesis: (Omega). V = (Omega). W
consider A being Basis of W;
consider B being Basis of V such that
A2: A c= B by Th17;
A3: card A = dim V by A1, Def3
.= card B by Def3 ;
( A c= the carrier of W & the carrier of W c= the carrier of V ) by RLSUB_1:def 2;
then reconsider A' = A as finite Subset of V by Th24, XBOOLE_1:1;
reconsider B' = B as finite Subset of V by Th24;

A4: now

assume A <> B ; :: thesis: contradiction
then A c< B by A2, XBOOLE_0:def 8;
then card A' < card B' by CARD_2:67;
hence contradiction by A3; :: thesis: verum

end;

reconsider A = A as Subset of W ;
reconsider B = B as Subset of V ;
(Omega). V = RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) by RLSUB_1:def 4
.= Lin B by RLVECT_3:def 3
.= Lin A by A4, Th21
.= RLSStruct(# the carrier of W,the U2 of W,the U5 of W,the Mult of W #) by RLVECT_3:def 3
.= (Omega). W by RLSUB_1:def 4 ;
hence (Omega). V = (Omega). W ; :: thesis: verum

end;

assume (Omega). V = (Omega). W ; :: thesis: dim V = dim W
then A5: RLSStruct(# the carrier of V,the U2 of V,the U5 of V,the Mult of V #) = (Omega). W by RLSUB_1:def 4
.= RLSStruct(# the carrier of W,the U2 of W,the U5 of W,the Mult of W #) by RLSUB_1:def 4 ;
consider A being finite Subset of V such that
A6: A is Basis of V by Def1;
consider B being finite Subset of W such that
A7: B is Basis of W by Def1;
A8: A is linearly-independent by A6, RLVECT_3:def 3;
A9: B is linearly-independent by A7, RLVECT_3:def 3;
A10: Lin A = RLSStruct(# the carrier of W,the U2 of W,the U5 of W,the Mult of W #) by A5, A6, RLVECT_3:def 3
.= Lin B by A7, RLVECT_3:def 3 ;
reconsider A = A as Subset of V ;
reconsider B = B as Subset of W ;
dim V = card A by A6, Def3
.= dim (Lin B) by A8, A10, Th30
.= card B by A9, Th30
.= dim W by A7, Def3 ;
hence dim V = dim W ; :: thesis: verum