let V be Z_Module; :: thesis: ( V is torsion-free iff torsion_part V = (0). V )
set W = torsion_part V;

hereby :: thesis: ( torsion_part V = (0). V implies V is torsion-free )

assume A1: V is torsion-free ; :: thesis: torsion_part V = (0). V
for x being object st x in the carrier of (torsion_part V) holds
x in {(0. V)}

proof

let x be object ; :: thesis: ( x in the carrier of (torsion_part V) implies x in {(0. V)} )
assume B11: x in the carrier of (torsion_part V) ; :: thesis: x in {(0. V)}
then B1: x in torsion_part V ;
reconsider xx = x as VECTOR of V by B11, ZMODUL01:25;
xx is torsion by B1, LmTP1;
then x = 0. V by A1;
hence x in {(0. V)} by TARSKI:def 1; :: thesis: verum

end;

then A3: the carrier of (torsion_part V) c= {(0. V)} ;
0. V in torsion_part V by ZMODUL01:33;
then {(0. V)} c= the carrier of (torsion_part V) by ZFMISC_1:31;
hence torsion_part V = (0). V by A3, XBOOLE_0:def 10, VECTSP_4:def 3; :: thesis: verum

end;

assume torsion_part V = (0). V ; :: thesis: V is torsion-free
then A2: the carrier of (torsion_part V) = {(0. V)} by VECTSP_4:def 3;
for v being VECTOR of V st v is torsion holds
v = 0. V

proof

let v be VECTOR of V; :: thesis: ( v is torsion implies v = 0. V )
assume v is torsion ; :: thesis: v = 0. V
then v in torsion_part V by LmTP1;
hence v = 0. V by A2, TARSKI:def 1; :: thesis: verum

end;

hence V is torsion-free ; :: thesis: verum