theorem ThDivisibleX1: :: ZMODUL08:30

for V being torsion-free Z_Module holds
( ( for v being Vector of (Z_MQ_VectSp V) holds v is Vector of (DivisibleMod V) ) & ( for v being Vector of (DivisibleMod V) holds v is Vector of (Z_MQ_VectSp V) ) & 0. (DivisibleMod V) = 0. (Z_MQ_VectSp V) )