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;

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;