let V be Z_Module; :: thesis: for v being Vector of V holds
( v is torsion iff v in torsion_part V )
let v be Vector of V; :: thesis: ( v is torsion iff v in torsion_part V )
set W = torsion_part V;

hereby :: thesis: ( v in torsion_part V implies v is torsion )

assume v is torsion ; :: thesis: v in torsion_part V
then v in { v where v is Vector of V : v is torsion } ;
hence v in torsion_part V by defTorsionPart; :: thesis: verum

end;

assume v in torsion_part V ; :: thesis: v is torsion
then v in { v where v is Vector of V : v is torsion } by defTorsionPart;
then consider vv being Vector of V such that
A2: ( vv = v & vv is torsion ) ;
thus v is torsion by A2; :: thesis: verum