let GF be Field; :: thesis: for V being finite-dimensional VectSp of GF
for W being Subspace of V holds
( dim V = dim W iff (Omega). V = (Omega). W )
let V be finite-dimensional VectSp of GF; :: 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 MATRLIN:def 1;

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

set A = the Basis of W;
consider B being Basis of V such that
A2: the Basis of W c= B by Th13;
the carrier of W c= the carrier of V by VECTSP_4:def 2;
then reconsider A9 = the Basis of W as finite Subset of V by XBOOLE_1:1;
reconsider B9 = B as finite Subset of V ;
assume dim V = dim W ; :: thesis: (Omega). V = (Omega). W
then A3: card the Basis of W = dim V by Def1
.= card B by Def1 ;

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

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;

reconsider B = B as Subset of V ;
reconsider A = the Basis of W as Subset of W ;
(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 B by VECTSP_7:def 3
.= Lin A by A4, Th17
.= ModuleStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by VECTSP_7:def 3
.= (Omega). W by VECTSP_4:def 4 ;
hence (Omega). V = (Omega). W ; :: thesis: verum

end;

consider B being finite Subset of W such that
A5: B is Basis of W by MATRLIN:def 1;
A6: A is linearly-independent by A1, VECTSP_7:def 3;
assume (Omega). V = (Omega). W ; :: thesis: dim V = dim W
then ModuleStr(# the carrier of V, the U5 of V, the ZeroF of V, the lmult of V #) = (Omega). W by VECTSP_4:def 4
.= ModuleStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by VECTSP_4:def 4 ;
then A7: Lin A = ModuleStr(# the carrier of W, the U5 of W, the ZeroF of W, the lmult of W #) by A1, VECTSP_7:def 3
.= Lin B by A5, VECTSP_7:def 3 ;
A8: B is linearly-independent by A5, VECTSP_7:def 3;
reconsider B = B as Subset of W ;
reconsider A = A as Subset of V ;
dim V = card A by A1, Def1
.= dim (Lin B) by A6, A7, Th26
.= card B by A8, Th26
.= dim W by A5, Def1 ;
hence dim V = dim W ; :: thesis: verum