let V be Z_Module; :: thesis: for z1, z2 being Element of V
for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
let z1, z2 be Element of V; :: thesis: for i1, i2 being Element of INT.Ring st V is Mult-cancelable holds
( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )
let i1, i2 be Element of INT.Ring; :: thesis: ( V is Mult-cancelable implies ( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) )
assume AS: V is Mult-cancelable ; :: thesis: ( [[z1,i1],[z2,i2]] in EQRZM V iff ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) )

hereby :: thesis: ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 implies [[z1,i1],[z2,i2]] in EQRZM V )

assume [[z1,i1],[z2,i2]] in EQRZM V ; :: thesis: ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 )
then consider zz1, zz2 being Element of V, ii1, ii2 being Element of INT.Ring such that
P2: ( [z1,i1] = [zz1,ii1] & [z2,i2] = [zz2,ii2] & ii1 <> 0 & ii2 <> 0 & ii2 * zz1 = ii1 * zz2 ) by AS, defEQRZM;
( z1 = zz1 & i1 = ii1 & z2 = zz2 & i2 = ii2 ) by P2, XTUPLE_0:1;
hence ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) by P2; :: thesis: verum

end;

assume A2: ( i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ; :: thesis: [[z1,i1],[z2,i2]] in EQRZM V
then A21: ( not i1 in {0} & not i2 in {0} ) by TARSKI:def 1;
( i1 in INT \ {0} & i2 in INT \ {0} ) by XBOOLE_0:def 5, A21;
then ( [z1,i1] in [: the carrier of V,(INT \ {0}):] & [z2,i2] in [: the carrier of V,(INT \ {0}):] ) by ZFMISC_1:87;
hence [[z1,i1],[z2,i2]] in EQRZM V by A2, AS, defEQRZM; :: thesis: verum