for V being non trivial torsion-free Z_Module
for v being non zero Vector of V
for A being Subset of V
for a being Element of INT.Ring st a in NAT & A is linearly-independent & a > 0 & a * v in Lin A holds
ex L being Linear_Combination of A ex u being Vector of V st
( a * v = Sum L & u in A & L . u <> 0 )