let V be free finite-rank Z_Module; :: thesis: for I being linearly-independent Subset of V holds I is finite
let I be linearly-independent Subset of V; :: thesis: I is finite
set IV = the Basis of V;
card I c= card the Basis of V by ZMODUL04:20;
hence I is finite ; :: thesis: verum