theorem ThDivisibleX2: :: ZMODUL08:31

for V being torsion-free Z_Module holds
( ( for x, y being Vector of (DivisibleMod V)
for v, u being Vector of (Z_MQ_VectSp V) st x = v & y = u holds
x + y = v + u ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for a being Element of INT.Ring
for aq being Element of F_Rat st z = w & a = aq holds
a * z = aq * w ) & ( for z being Vector of (DivisibleMod V)
for w being Vector of (Z_MQ_VectSp V)
for aq being Element of F_Rat
for a being Element of INT.Ring st a <> 0 & aq = a & a * z = aq * w holds
z = w ) & ( for x being Vector of (DivisibleMod V)
for v being Vector of (Z_MQ_VectSp V)
for r being Element of F_Rat
for m, n being Element of INT.Ring
for mi, ni being Integer st m = mi & n = ni & x = v & r <> 0. F_Rat & n <> 0 & r = mi / ni holds
ex y being Vector of (DivisibleMod V) st
( x = n * y & r * v = m * y ) ) )