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