let V be Z_Module; :: thesis: for A being finite linearly-independent Subset of V holds card A = rank (Lin A)
let A be finite linearly-independent Subset of V; :: thesis: card A = rank (Lin A)
set W = Lin A;

now :: thesis: for x being object st x in A holds
x in the carrier of (Lin A)

let x be object ; :: 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 ZMODUL02:65;
hence x in the carrier of (Lin A) ; :: thesis: verum

end;

then reconsider B = A as finite linearly-independent Subset of (Lin A) by ZMODUL03:16, TARSKI:def 3;
Lin A = Lin B by ZMODUL03:20;
then reconsider B = B as Basis of (Lin A) by VECTSP_7:def 3;
card B = rank (Lin A) by ZMODUL03:def 5;
hence card A = rank (Lin A) ; :: thesis: verum