defpred S1[ object , object ] means ( $1 in E & $2 in E & ex k, l being Nat st (iter (f,k)) . $1 = (iter (f,l)) . $2 );
A1:
now for x being object st x in E holds
S1[x,x]let x be
object ;
( x in E implies S1[x,x] )A2:
(iter (f,0)) . x = (iter (f,0)) . x
;
assume
x in E
;
S1[x,x]hence
S1[
x,
x]
by A2;
verum end;
A3:
now for x, y, z being object st S1[x,y] & S1[y,z] holds
S1[x,z]let x,
y,
z be
object ;
( S1[x,y] & S1[y,z] implies S1[x,z] )assume that A4:
S1[
x,
y]
and A5:
S1[
y,
z]
;
S1[x,z]consider k,
l being
Nat such that A6:
(iter (f,k)) . x = (iter (f,l)) . y
by A4;
consider m,
n being
Nat such that A7:
(iter (f,m)) . y = (iter (f,n)) . z
by A5;
A8:
dom (iter (f,m)) = E
by FUNCT_2:52;
A9:
dom (iter (f,l)) = E
by FUNCT_2:52;
A10:
dom (iter (f,k)) = E
by FUNCT_2:52;
A11:
dom (iter (f,n)) = E
by FUNCT_2:52;
(iter (f,(k + m))) . x =
((iter (f,m)) * (iter (f,k))) . x
by FUNCT_7:77
.=
(iter (f,m)) . ((iter (f,l)) . y)
by A4, A6, A10, FUNCT_1:13
.=
((iter (f,m)) * (iter (f,l))) . y
by A4, A9, FUNCT_1:13
.=
(iter (f,(m + l))) . y
by FUNCT_7:77
.=
((iter (f,l)) * (iter (f,m))) . y
by FUNCT_7:77
.=
(iter (f,l)) . ((iter (f,n)) . z)
by A4, A7, A8, FUNCT_1:13
.=
((iter (f,l)) * (iter (f,n))) . z
by A5, A11, FUNCT_1:13
.=
(iter (f,(l + n))) . z
by FUNCT_7:77
;
hence
S1[
x,
z]
by A4, A5;
verum end;
A12:
for x, y being object st S1[x,y] holds
S1[y,x]
;
consider EqR being Equivalence_Relation of E such that
A13:
for x, y being object holds
( [x,y] in EqR iff ( x in E & y in E & S1[x,y] ) )
from EQREL_1:sch 1(A1, A12, A3);
take
EqR
; for x, y being set st x in E & y in E holds
( [x,y] in EqR iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y )
let x, y be set ; ( x in E & y in E implies ( [x,y] in EqR iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y ) )
assume
( x in E & y in E )
; ( [x,y] in EqR iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y )
hence
( [x,y] in EqR iff ex k, l being Nat st (iter (f,k)) . x = (iter (f,l)) . y )
by A13; verum