let G be Z_Module; :: thesis: for i, w being Element of INT
for v being Element of G st G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w
let i, w be Element of INT ; :: thesis: for v being Element of G st G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w
let v be Element of G; :: thesis: ( G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w implies i * v = i * w )
assume A1: ( G = Z_ModuleStruct(# the carrier of INT.Ring, the ZeroF of INT.Ring, the addF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w ) ; :: thesis: i * v = i * w
reconsider r = v as Element of INT.Ring by A1;

per cases ( 0 <= i or not 0 <= i ) ;

suppose 0 <= i ; :: thesis: i * v = i * w

then reconsider n = i as Element of NAT by INT_1:3;
thus i * v = n * r by A1, ZMODUL01:def 23
.= i * w by A1, Lm1 ; :: thesis: verum

end;

suppose A2: not 0 <= i ; :: thesis: i * v = i * w

then reconsider n = - i as Element of NAT by INT_1:3;
thus i * v = n * (- r) by A1, A2, ZMODUL01:def 23
.= (- i) * (- r) by Lm1
.= i * w by A1 ; :: thesis: verum

end;

end;