theorem ThDM1: :: ZMODUL08:29

for V being torsion-free Z_Module
for v being Vector of (DivisibleMod V) ex a being Element of INT.Ring st
( a <> 0 & a * v in EMbedding V )