let V be Z_Module; :: thesis: ( V is torsion-free iff (Omega). V is torsion-free )
thus ( V is torsion-free implies (Omega). V is torsion-free ) ; :: thesis: ( (Omega). V is torsion-free implies V is torsion-free )
assume A1: (Omega). V is torsion-free ; :: thesis: V is torsion-free
for v being Vector of V st v <> 0. V holds
not v is torsion

proof

let v be Vector of V; :: thesis: ( v <> 0. V implies not v is torsion )
assume B1: v <> 0. V ; :: thesis: not v is torsion
reconsider vv = v as Vector of ((Omega). V) ;
B2: not vv is torsion by A1, B1;
for i being Element of INT.Ring st i <> 0. INT.Ring holds
i * v <> 0. V

proof

let i be Element of INT.Ring; :: thesis: ( i <> 0. INT.Ring implies i * v <> 0. V )
assume C1: i <> 0. INT.Ring ; :: thesis: i * v <> 0. V
i * vv <> 0. ((Omega). V) by B2, C1;
hence i * v <> 0. V ; :: thesis: verum

end;

hence not v is torsion ; :: thesis: verum

end;

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