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
A33: dom f1 = dom f and
A34: 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
A35: dom f2 = dom f and
A36: 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 :: thesis: for a being object st a in dom f holds
f1 . a = f2 . a

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

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

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

hence f1 . a = x by A34, A37
.= f2 . a by A36, A37, A38 ;
:: thesis: verum

end;

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

then consider y being object such that
A39: y in f orbit a and
A40: y nin A ;
A41: ex n1 being Element of NAT st
( y = (iter (f,n1)) . a & a in dom (iter (f,n1)) ) by A39;
defpred S₂[ Nat] means (iter (f,$1)) . a nin A;
A42: ex n being Nat st S₂[n] by A40, A41;
consider n being Nat such that
A43: S₂[n] and
A44: for m being Nat st S₂[m] holds
n <= m from NAT_1:sch 5(A42);
A45: for i being Nat st i < n holds
(iter (f,i)) . a in A by A44;
hence f1 . a = (iter (f,n)) . a by A34, A37, A43
.= f2 . a by A36, A37, A43, A45 ;
:: thesis: verum

end;

end;

end;

hence f1 = f2 by A33, A35; :: thesis: verum