defpred S₁[ 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 :: thesis: for x being object st x in E holds
S₁[x,x]

let x be object ; :: thesis: ( x in E implies S₁[x,x] )
A2: (iter (f,0)) . x = (iter (f,0)) . x ;
assume x in E ; :: thesis: S₁[x,x]
hence S₁[x,x] by A2; :: thesis: verum

end;

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

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[y,z] implies S₁[x,z] )
assume that
A4: S₁[x,y] and
A5: S₁[y,z] ; :: thesis: S₁[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 S₁[x,z] by A4, A5; :: thesis: verum

end;

A12: for x, y being object st S₁[x,y] holds
S₁[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 & S₁[x,y] ) ) from EQREL_1:sch 1(A1, A12, A3);
take EqR ; :: thesis: 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 ; :: thesis: ( 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 ) ; :: thesis: ( [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; :: thesis: verum