let V be Z_Module; :: thesis: ( V is Mult-cancelable iff V is torsion-free )

hereby :: thesis: ( V is torsion-free implies V is Mult-cancelable )

assume V is Mult-cancelable ; :: thesis: V is torsion-free
then for v being Vector of V st v <> 0. V holds
not v is torsion ;
hence V is torsion-free ; :: thesis: verum

end;

assume AS: V is torsion-free ; :: thesis: V is Mult-cancelable
for i being Element of INT.Ring
for v being Vector of V st i <> 0. INT.Ring & v <> 0. V holds
i * v <> 0. V

proof

let i be Element of INT.Ring; :: thesis: for v being Vector of V st i <> 0. INT.Ring & v <> 0. V holds
i * v <> 0. V
let v be Vector of V; :: thesis: ( i <> 0. INT.Ring & v <> 0. V implies i * v <> 0. V )
assume A1: ( i <> 0. INT.Ring & v <> 0. V ) ; :: thesis: i * v <> 0. V
then not v is torsion by AS;
hence i * v <> 0. V by A1; :: thesis: verum

end;

hence V is Mult-cancelable ; :: thesis: verum