:: deftheorem defTorsionPart defines torsion_part ZMODUL07:def 1 :
for V being LeftMod of INT.Ring
for b₂ being strict Subspace of V holds
( b₂ = torsion_part V iff the carrier of b₂ = { v where v is Vector of V : v is torsion } );