let V be finite-dimensional RealLinearSpace; :: thesis: for A being Subset of V st A is linearly-independent holds
card A = dim (Lin A)
let A be Subset of V; :: thesis: ( A is linearly-independent implies card A = dim (Lin A) )
assume A1: A is linearly-independent ; :: thesis: card A = dim (Lin A)
set W = Lin A;

now

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

end;

then reconsider B = A as linearly-independent Subset of (Lin A) by A1, Th16, TARSKI:def 3;
Lin A = Lin B by Th21;
then reconsider B = B as Basis of Lin A by RLVECT_3:def 3;
card B = dim (Lin A) by Def3;
hence card A = dim (Lin A) ; :: thesis: verum