defpred S₁[ object , object ] means ex z1, z2 being Element of V ex i1, i2 being Element of INT.Ring st
( $1 = [z1,i1] & $2 = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 );
A1: for x being object st x in [: the carrier of V,(INT \ {0}):] holds
S₁[x,x]

proof

let x be object ; :: thesis: ( x in [: the carrier of V,(INT \ {0}):] implies S₁[x,x] )
assume x in [: the carrier of V,(INT \ {0}):] ; :: thesis: S₁[x,x]
then consider z1, i1 being object such that
A11: ( z1 in the carrier of V & i1 in INT \ {0} & x = [z1,i1] ) by ZFMISC_1:def 2;
reconsider z1 = z1 as Element of V by A11;
A12: ( i1 in INT & not i1 in {0} ) by XBOOLE_0:def 5, A11;
reconsider i1 = i1 as Integer by A11;
reconsider i1 = i1 as Element of INT.Ring by A11;
( i1 <> 0 & i1 <> 0 & i1 * z1 = i1 * z1 ) by A12, TARSKI:def 1;
hence S₁[x,x] by A11; :: thesis: verum

end;

A2: for x, y being object st S₁[x,y] holds
S₁[y,x] ;
A3: for x, y, z being object st S₁[x,y] & S₁[y,z] holds
S₁[x,z]

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[y,z] implies S₁[x,z] )
assume A31: ( S₁[x,y] & S₁[y,z] ) ; :: thesis: S₁[x,z]
then consider z1, z2 being Element of V, i1, i2 being Element of INT.Ring such that
A32: ( x = [z1,i1] & y = [z2,i2] & i1 <> 0 & i2 <> 0 & i2 * z1 = i1 * z2 ) ;
consider z3, z4 being Element of V, i3, i4 being Element of INT.Ring such that
A33: ( y = [z3,i3] & z = [z4,i4] & i3 <> 0 & i4 <> 0 & i4 * z3 = i3 * z4 ) by A31;
A34: ( z2 = z3 & i2 = i3 ) by A32, A33, XTUPLE_0:1;
i2 * (i4 * z1) = (i2 * i4) * z1 by VECTSP_1:def 16
.= (i4 * i2) * z1
.= i4 * (i2 * z1) by VECTSP_1:def 16
.= i4 * (i1 * z2) by A32
.= (i4 * i1) * z2 by VECTSP_1:def 16
.= (i1 * i4) * z2
.= i1 * (i4 * z2) by VECTSP_1:def 16
.= (i1 * i2) * z4 by A33, A34, VECTSP_1:def 16
.= (i2 * i1) * z4
.= i2 * (i1 * z4) by VECTSP_1:def 16 ;
hence S₁[x,z] by AS, A32, A33, ZMODUL01:10; :: thesis: verum

end;

consider EqR being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] such that
A4: for x, y being object holds
( [x,y] in EqR iff ( x in [: the carrier of V,(INT \ {0}):] & y in [: the carrier of V,(INT \ {0}):] & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A2, A3);
take EqR ; :: thesis: for S, T being object holds
( [S,T] in EqR 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 ) ) )
thus for S, T being object holds
( [S,T] in EqR 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 A4; :: thesis: verum