let K be Field; :: thesis: for V1 being VectSp of K
for A being finite Subset of V1 st dim (Lin A) = card A holds
A is linearly-independent
let V1 be VectSp of K; :: thesis: for A being finite Subset of V1 st dim (Lin A) = card A holds
A is linearly-independent
let A be finite Subset of V1; :: thesis: ( dim (Lin A) = card A implies A is linearly-independent )
assume A1: dim (Lin A) = card A ; :: thesis: A is linearly-independent
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
A2: B c= A9 and
A3: B is linearly-independent and
A4: Lin B = Lin A by VECTSP_7:18;
reconsider B = B as finite Subset of (Lin A) by A2;
B is Basis of (Lin A) by A3, A4, VECTSP_7:def 3;
then reconsider L = Lin A as finite-dimensional VectSp of K by MATRLIN:def 1;
card A = dim L by A1
.= card B by A3, A4, VECTSP_9:26 ;
then A = B by A2, CARD_2:102;
hence A is linearly-independent by A3, VECTSP_9:11; :: thesis: verum