theorem LmTP1: :: ZMODUL07:11

for V being Z_Module
for v being Vector of V holds
( v is torsion iff v in torsion_part V )