let V be Z_Module; :: thesis: for v being Vector of V st not v is torsion holds
not - v is torsion
let v be Vector of V; :: thesis: ( not v is torsion implies not - v is torsion )
assume A1: not v is torsion ; :: thesis: not - v is torsion
assume - v is torsion ; :: thesis: contradiction
then consider i being Element of INT.Ring such that
A3: ( i <> 0 & i * (- v) = 0. V ) ;
(- i) * v = 0. V by A3, ZMODUL01:5;
hence contradiction by A1, A3; :: thesis: verum