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