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