defpred S_{1}[ 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_{1}[x,x]
_{1}[x,y] holds

S_{1}[y,x]
;

A3: for x, y, z being object st S_{1}[x,y] & S_{1}[y,z] holds

S_{1}[x,z]

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_{1}[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

( $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

proof

A2:
for x, y being object st S
let x be object ; :: thesis: ( x in [: the carrier of V,(INT \ {0}):] implies S_{1}[x,x] )

assume x in [: the carrier of V,(INT \ {0}):] ; :: thesis: S_{1}[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_{1}[x,x]
by A11; :: thesis: verum

end;assume x in [: the carrier of V,(INT \ {0}):] ; :: thesis: S

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

S

A3: for x, y, z being object st S

S

proof

consider EqR being Equivalence_Relation of [: the carrier of V,(INT \ {0}):] such that
let x, y, z be object ; :: thesis: ( S_{1}[x,y] & S_{1}[y,z] implies S_{1}[x,z] )

assume A31: ( S_{1}[x,y] & S_{1}[y,z] )
; :: thesis: S_{1}[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_{1}[x,z]
by AS, A32, A33, ZMODUL01:10; :: thesis: verum

end;assume A31: ( S

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

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

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