theorem :: ZMODUL07:12

for V being Z_Module holds
( V is torsion-free iff torsion_part V = (0). V )