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 )

consider A being finite Subset of V such that

A1: A is Basis of V by Def1;

A5: B is Basis of W by Def1;

A6: A is linearly-independent by A1, RLVECT_3:def 3;

assume (Omega). V = (Omega). W ; :: thesis: dim V = dim W

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

.= RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by RLSUB_1:def 4 ;

then A7: Lin A = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by A1, RLVECT_3:def 3

.= Lin B by A5, RLVECT_3:def 3 ;

A8: B is linearly-independent by A5, RLVECT_3:def 3;

reconsider B = B as Subset of W ;

reconsider A = A as Subset of V ;

dim V = card A by A1, Def2

.= dim (Lin B) by A6, A7, Th29

.= card B by A8, Th29

.= dim W by A5, Def2 ;

hence dim V = dim W ; :: thesis: verum

( 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 )

consider A being finite Subset of V such that

A1: A is Basis of V by Def1;

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

consider B being finite Subset of W such that set A = the Basis of W;

consider B being Basis of V such that

A2: the Basis of W c= B by Th16;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = the Basis of W as finite Subset of V by Th23, XBOOLE_1:1;

reconsider B9 = B as finite Subset of V by Th23;

assume dim V = dim W ; :: thesis: (Omega). V = (Omega). W

then A3: card the Basis of W = dim V by Def2

.= card B by Def2 ;

reconsider A = the Basis of W as Subset of W ;

(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 B by RLVECT_3:def 3

.= Lin A by A4, Th20

.= RLSStruct(# the carrier of W, the ZeroF 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;consider B being Basis of V such that

A2: the Basis of W c= B by Th16;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then reconsider A9 = the Basis of W as finite Subset of V by Th23, XBOOLE_1:1;

reconsider B9 = B as finite Subset of V by Th23;

assume dim V = dim W ; :: thesis: (Omega). V = (Omega). W

then A3: card the Basis of W = dim V by Def2

.= card B by Def2 ;

A4: now :: thesis: not the Basis of W <> B

reconsider B = B as Subset of V ;assume
the Basis of W <> B
; :: thesis: contradiction

then the Basis of W c< B by A2, XBOOLE_0:def 8;

then card A9 < card B9 by CARD_2:48;

hence contradiction by A3; :: thesis: verum

end;then the Basis of W c< B by A2, XBOOLE_0:def 8;

then card A9 < card B9 by CARD_2:48;

hence contradiction by A3; :: thesis: verum

reconsider A = the Basis of W as Subset of W ;

(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 B by RLVECT_3:def 3

.= Lin A by A4, Th20

.= RLSStruct(# the carrier of W, the ZeroF 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

A5: B is Basis of W by Def1;

A6: A is linearly-independent by A1, RLVECT_3:def 3;

assume (Omega). V = (Omega). W ; :: thesis: dim V = dim W

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

.= RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by RLSUB_1:def 4 ;

then A7: Lin A = RLSStruct(# the carrier of W, the ZeroF of W, the U5 of W, the Mult of W #) by A1, RLVECT_3:def 3

.= Lin B by A5, RLVECT_3:def 3 ;

A8: B is linearly-independent by A5, RLVECT_3:def 3;

reconsider B = B as Subset of W ;

reconsider A = A as Subset of V ;

dim V = card A by A1, Def2

.= dim (Lin B) by A6, A7, Th29

.= card B by A8, Th29

.= dim W by A5, Def2 ;

hence dim V = dim W ; :: thesis: verum