theorem LMEQR001: :: ZMODUL04:3

for V being Z_Module
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 ) )