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

per cases ( ai > 0 or ai < 0 ) by B1;

suppose ai > 0 ; :: thesis: |.ai.| * v in Lin A

hence |.ai.| * v in Lin A by B1, ABSVALUE:def 1; :: thesis: verum

end;

suppose ai < 0 ; :: thesis: |.ai.| * v in Lin A

then |.ai.| = - ai by ABSVALUE:def 1;
then |.ai.| * v = - (ai * v) by ZMODUL01:16;
hence |.ai.| * v in Lin A by B1, ZMODUL01:38; :: thesis: verum

end;

end;

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