let G be Z_Module; :: thesis: for i being Element of INT.Ring
for w being Element of INT
for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w
let i be Element of INT.Ring; :: thesis: for w being Element of INT
for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w
let w be Element of INT ; :: thesis: for v being Element of G st G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w holds
i * v = i * w
let v be Element of G; :: thesis: ( G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF of INT.Ring,(Int-mult-left INT.Ring) #) & v = w implies i * v = i * w )
assume A1: ( G = ModuleStr(# the carrier of INT.Ring, the addF of INT.Ring, the ZeroF 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 20
.= 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 20
.= (- i) * (- r) by Lm1
.= i * w by A1 ; :: thesis: verum
end;
end;