let GF be Field; :: thesis: for V being finite-dimensional VectSp of finite-dimensional
for W being Subspace of V holds dim W <= dim V
let V be finite-dimensional VectSp of finite-dimensional ; :: thesis: for W being Subspace of V holds dim W <= dim V
let W be Subspace of V; :: thesis: dim W <= dim V
consider A being Basis of W;
reconsider A = A as Subset of ;
A1: dim W = card A by Def2;
A is linearly-independent by VECTSP_7:def 3;
then reconsider B = A as linearly-independent Subset of by Th15;
reconsider A' = B as finite Subset of by Th24;
reconsider V' = V as VectSp of ;
consider I being Basis of V';
A2: Lin I = VectSpStr(# the carrier of V',the U5 of V',the U2 of V',the lmult of V' #) by VECTSP_7:def 3;
reconsider I = I as finite Subset of by Th24;
card A' <= card I by A2, Th23;
hence dim W <= dim V by A1, Def2; :: thesis: verum