defpred S₁[ set , set ] means ( $1 in E & $2 in E & ex k, l being Element of NAT st (iter f,k) . $1 = (iter f,l) . $2 );

A1: now

let x be set ; :: 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

let x, y, z be set ; :: 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 Element of NAT such that
A6: (iter f,k) . x = (iter f,l) . y by A4;
consider m, n being Element of NAT such that
A7: (iter f,m) . y = (iter f,n) . z by A5;
A8: dom (iter f,m) = E by FUNCT_2:67;
A9: dom (iter f,l) = E by FUNCT_2:67;
A10: dom (iter f,k) = E by FUNCT_2:67;
A11: dom (iter f,n) = E by FUNCT_2:67;
(iter f,(k + m)) . x = ((iter f,m) * (iter f,k)) . x by FUNCT_7:79
.= (iter f,m) . ((iter f,l) . y) by A4, A6, A10, FUNCT_1:23
.= ((iter f,m) * (iter f,l)) . y by A4, A9, FUNCT_1:23
.= (iter f,(m + l)) . y by FUNCT_7:79
.= ((iter f,l) * (iter f,m)) . y by FUNCT_7:79
.= (iter f,l) . ((iter f,n) . z) by A4, A7, A8, FUNCT_1:23
.= ((iter f,l) * (iter f,n)) . z by A5, A11, FUNCT_1:23
.= (iter f,(l + n)) . z by FUNCT_7:79 ;
hence S₁[x,z] by A4, A5; :: thesis: verum

end;

A12: for x, y being set st S₁[x,y] holds
S₁[y,x] ;
consider EqR being Equivalence_Relation of E such that
A13: for x, y being set 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 Element of 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 Element of 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 Element of NAT st (iter f,k) . x = (iter f,l) . y )
hence ( [x,y] in EqR iff ex k, l being Element of NAT st (iter f,k) . x = (iter f,l) . y ) by A13; :: thesis: verum