theorem :: ZMODUL08:37

for V being Z_Module 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 ) ) )