theorem LMEQR003: :: ZMODUL04:4

for V being Z_Module
for z being Element of V
for i, n being Element of INT.Ring st i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable holds
Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)])