:: deftheorem defEQRZM defines EQRZM ZMODUL04:def 1 :
for V being Z_Module st V is Mult-cancelable holds
for b₂ being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] holds
( b₂ = EQRZM V iff for S, T being object holds
( [S,T] in b₂ iff ( S in [: the carrier of V,(INT \ {0}):] & T in [: the carrier of V,(INT \ {0}):] & ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( S = [z1,i1] & T = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ) ) );