let f1, f2 be Function; :: thesis: ( dom f1 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies f1 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
f1 . a = (iter f,n) . a ) ) ) & dom f2 = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies f2 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
f2 . a = (iter f,n) . a ) ) ) implies f1 = f2 )
assume that
A24: dom f1 = dom f and
A25: for a being set st a in dom f holds
( ( f orbit a c= A implies f1 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
f1 . a = (iter f,n) . a ) ) and
A26: dom f2 = dom f and
A27: for a being set st a in dom f holds
( ( f orbit a c= A implies f2 . a = x ) & ( for n being Nat st (iter f,n) . a nin A & ( for i being Nat st i < n holds
(iter f,i) . a in A ) holds
f2 . a = (iter f,n) . a ) ) ; :: thesis: f1 = f2

now

let a be set ; :: thesis: ( a in dom f implies f1 . b₁ = f2 . b₁ )
assume A28: a in dom f ; :: thesis: f1 . b₁ = f2 . b₁

per cases ( f orbit a c= A or not f orbit a c= A ) ;

suppose A29: f orbit a c= A ; :: thesis: f1 . b₁ = f2 . b₁

hence f1 . a = x by A25, A28
.= f2 . a by A27, A28, A29 ;
:: thesis: verum

end;

suppose not f orbit a c= A ; :: thesis: f1 . b₁ = f2 . b₁

then consider y being set such that
A30: ( y in f orbit a & y nin A ) by TARSKI:def 3;
consider n1 being Element of NAT such that
A31: ( y = (iter f,n1) . a & a in dom (iter f,n1) ) by A30;
defpred S₂[ Nat] means (iter f,$1) . a nin A;
A32: ex n being Nat st S₂[n] by A30, A31;
consider n being Nat such that
A33: S₂[n] and
A34: for m being Nat st S₂[m] holds
n <= m from NAT_1:sch 5(A32);
A35: for i being Nat st i < n holds
(iter f,i) . a in A by A34;
hence f1 . a = (iter f,n) . a by A25, A28, A33
.= f2 . a by A27, A28, A33, A35 ;
:: thesis: verum

end;

end;

end;

hence f1 = f2 by A24, A26, FUNCT_1:9; :: thesis: verum