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

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