theorem Th2: :: ZMODUL03:2

for G being Z_Module
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