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 ;
( z1 = zz1 & i1 = ii1 & z2 = zz2 & i2 = ii2 ) by ;
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 & not i2 in ) by TARSKI:def 1;
( i1 in INT \ & i2 in INT \ ) by ;
then ( [z1,i1] in [: the carrier of V,():] & [z2,i2] in [: the carrier of V,():] ) by ZFMISC_1:87;
hence [[z1,i1],[z2,i2]] in EQRZM V by ; :: thesis: verum