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