let V be Z_Module; :: thesis: 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)])
let z be Element of V; :: thesis: 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)])
let i, n be Element of INT.Ring; :: thesis: ( i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable implies Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)]) )
assume AS: ( i <> 0. INT.Ring & n <> 0. INT.Ring & V is Mult-cancelable ) ; :: thesis: Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)])
then B61: not i in {0} by TARSKI:def 1;
i in INT \ {0} by XBOOLE_0:def 5, B61;
then X1: [z,i] in [: the carrier of V,(INT \ {0}):] by ZFMISC_1:87;
(n * i) * z = (i * n) * z
.= i * (n * z) by VECTSP_1:def 16 ;
then [[z,i],[(n * z),(n * i)]] in EQRZM V by AS, LMEQR001;
hence Class ((EQRZM V),[z,i]) = Class ((EQRZM V),[(n * z),(n * i)]) by X1, EQREL_1:35; :: thesis: verum