theorem :: ZMODUL08:18

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