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 )
proof
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;
hence EqR1 = EqR2 by Lm19, A3, A4; :: thesis: verum