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;

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

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)

then reconsider B = A as finite linearly-independent Subset of (Lin A) by ZMODUL03:16, TARSKI:def 3;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;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

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