let K be Field; :: thesis: for V being VectSp of K
for A being finite Subset of V holds dim (Lin A) <= card A
let V be VectSp of K; :: thesis: for A being finite Subset of V holds dim (Lin A) <= card A
let A be finite Subset of V; :: thesis: dim (Lin A) <= card A
set L = Lin A;
A c= the carrier of (Lin A)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in the carrier of (Lin A) )
assume x in A ; :: thesis: x in the carrier of (Lin A)
then x in Lin A by VECTSP_7:8;
hence x in the carrier of (Lin A) ; :: thesis: verum
end;
then reconsider A9 = A as Subset of (Lin A) ;
Lin A9 = Lin A by VECTSP_9:17;
then consider B being Subset of (Lin A) such that
A1: B c= A9 and
A2: ( B is linearly-independent & Lin B = Lin A ) by VECTSP_7:18;
reconsider B = B as finite Subset of (Lin A) by A1;
B is Basis of (Lin A) by A2, VECTSP_7:def 3;
then reconsider L = Lin A as finite-dimensional VectSp of K by MATRLIN:def 1;
( card B = dim L & Segm (card B) c= Segm (card A) ) by A1, A2, CARD_1:11, VECTSP_9:26;
hence dim (Lin A) <= card A by NAT_1:39; :: thesis: verum