let EqR1, EqR2 be Equivalence_Relation of [: the carrier of V,(INT \ {0}):]; :: thesis: ( ( for S, T being object holds

( [S,T] in EqR1 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 ) ) ) ) & ( for S, T being object holds

( [S,T] in EqR2 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 ) ) ) ) implies EqR1 = EqR2 )

assume A1: for S, T being object holds

( [S,T] in EqR1 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 ) ) ) ; :: thesis: ( ex S, T being object st

( ( [S,T] in EqR2 implies ( 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 ) ) ) implies ( 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 ) & not [S,T] in EqR2 ) ) or EqR1 = EqR2 )

assume A2: for S, T being object holds

( [S,T] in EqR2 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 ) ) ) ; :: thesis: EqR1 = EqR2

A3: for z being object st z in EqR1 holds

ex x, y being object st z = [x,y] by RELAT_1:def 1;

A4: for z being object st z in EqR2 holds

ex x, y being object st z = [x,y] by RELAT_1:def 1;

for x, y being object holds

( [x,y] in EqR1 iff [x,y] in EqR2 )

( [S,T] in EqR1 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 ) ) ) ) & ( for S, T being object holds

( [S,T] in EqR2 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 ) ) ) ) implies EqR1 = EqR2 )

assume A1: for S, T being object holds

( [S,T] in EqR1 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 ) ) ) ; :: thesis: ( ex S, T being object st

( ( [S,T] in EqR2 implies ( 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 ) ) ) implies ( 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 ) & not [S,T] in EqR2 ) ) or EqR1 = EqR2 )

assume A2: for S, T being object holds

( [S,T] in EqR2 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 ) ) ) ; :: thesis: EqR1 = EqR2

A3: for z being object st z in EqR1 holds

ex x, y being object st z = [x,y] by RELAT_1:def 1;

A4: for z being object st z in EqR2 holds

ex x, y being object st z = [x,y] by RELAT_1:def 1;

for x, y being object holds

( [x,y] in EqR1 iff [x,y] in EqR2 )

proof

hence
EqR1 = EqR2
by Lm19, A3, A4; :: thesis: verum
let S, T be object ; :: thesis: ( [S,T] in EqR1 iff [S,T] in EqR2 )

( [S,T] in EqR2 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 ) ) ) by A2;

hence ( [S,T] in EqR1 iff [S,T] in EqR2 ) by A1; :: thesis: verum

end;( [S,T] in EqR2 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 ) ) ) by A2;

hence ( [S,T] in EqR1 iff [S,T] in EqR2 ) by A1; :: thesis: verum