for V being non trivial free Z_Module
for v being non zero Vector of V ex a being Element of INT.Ring st
( a in NAT & ( for b being Element of INT.Ring
for u being Vector of V st b > a holds
v <> b * u ) )