let K be Field; :: thesis: for V being VectSp of
for A being finite Subset of holds dim (Lin A) <= card A
let V be VectSp of ; :: thesis: for A being finite Subset of holds dim (Lin A) <= card A
let A be finite Subset of ; :: thesis: dim (Lin A) <= card A
set L = Lin A;
A c= the carrier of (Lin A)

proof

let x be set ; :: 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:13;
hence x in the carrier of (Lin A) by STRUCT_0:def 5; :: thesis: verum

end;

then reconsider A' = A as Subset of ;
Lin A' = Lin A by VECTSP_9:21;
then consider B being Subset of such that
A1: B c= A' and
A2: ( B is linearly-independent & Lin B = Lin A ) by VECTSP_7:23;
reconsider B = B as finite Subset of by A1;
B is Basis of Lin A by A2, VECTSP_7:def 3;
then reconsider L = Lin A as finite-dimensional VectSp of finite-dimensional by MATRLIN:def 3;
( card B = dim L & card B c= card A ) by A1, A2, CARD_1:27, VECTSP_9:30;
hence dim (Lin A) <= card A by NAT_1:40; :: thesis: verum