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 ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )
let A be linearly-independent Subset of V; :: thesis: ex I being finite linearly-independent Subset of V ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )
consider I being finite Subset of V, a being Element of INT.Ring such that
P0: a <> 0. INT.Ring and
P1: A c= I and
P2: I is linearly-independent and
P3: for v being VECTOR of V holds a * v in Lin I by LmTF1A;
reconsider I = I as finite linearly-independent Subset of V by P2;
take I ; :: thesis: ex a being Element of INT.Ring st
( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )
take a ; :: thesis: ( a <> 0. INT.Ring & A c= I & a (*) V is Submodule of Lin I )
thus ( a <> 0. INT.Ring & A c= I ) by P0, P1; :: thesis: a (*) V is Submodule of Lin I
for v being VECTOR of V st v in a (*) V holds
v in Lin I

proof

let v be VECTOR of V; :: thesis: ( v in a (*) V implies v in Lin I )
assume v in a (*) V ; :: thesis: v in Lin I
then consider w being VECTOR of V such that
P4: v = a * w ;
thus v in Lin I by P3, P4; :: thesis: verum

end;

hence a (*) V is Submodule of Lin I by ZMODUL01:44; :: thesis: verum