let V be free finite-rank Z_Module; :: thesis: for A being linearly-independent Subset of V ex I being finite linearly-independent Subset of V st
( A c= I & rank V = card I )
let A be linearly-independent Subset of V; :: thesis: ex I being finite linearly-independent Subset of V st
( A c= I & rank V = card I )
consider I being finite linearly-independent Subset of V, a being Element of INT.Ring such that
A1: ( a <> 0 & A c= I & a (*) V is Submodule of Lin I ) by LmRankSX11;
take I ; :: thesis: ( A c= I & rank V = card I )
A3: V is free finite-rank Submodule of V by ZMODUL01:32;
rank (a (*) V) <= rank (Lin I) by A1, ZMODUL05:2;
then A2: rank V <= rank (Lin I) by A1, A3, ZMODUL06:52;
rank (Lin I) <= rank V by ZMODUL05:2;
then rank (Lin I) = rank V by A2, XXREAL_0:1;
hence ( A c= I & rank V = card I ) by A1, ZMODUL05:3; :: thesis: verum