theorem ThDivisible1: :: ZMODUL08:23

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