let V be Z_Module; :: thesis: ex A being Subset of V st
( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A ) ) )
{} the carrier of V is linearly-independent ;
then consider A being Subset of V such that
A1: ( {} c= A & A is linearly-independent & ( for v being Vector of V ex ai being Element of INT.Ring st
( ai <> 0 & ai * v in Lin A ) ) ) by ZMODUL07:2;
A2: for v being Vector of V ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A )
proof
let v be Vector of V; :: thesis: ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A )
consider ai being Element of INT.Ring such that
B1: ( ai <> 0 & ai * v in Lin A ) by A1;
set a = |.ai.|;
B2: |.ai.| <> 0 by B1, ABSVALUE:2;
N1: |.ai.| in NAT by COMPLEX1:46, INT_1:3;
|.ai.| * v in Lin A
proof
end;
hence ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A ) by N1, B2; :: thesis: verum
end;
take A ; :: thesis: ( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A ) ) )
thus ( A is linearly-independent & ( for v being Vector of V ex a being Element of INT.Ring st
( a in NAT & a > 0 & a * v in Lin A ) ) ) by A1, A2; :: thesis: verum