defpred S₂[ set ] means f orbit $1 c= A;
consider Z being set such that
A9: for a being set holds
( a in Z iff ( a in dom f & S₂[a] ) ) from XBOOLE_0:sch 1();
A10: Z c= dom f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin Z or not a nin dom f )
thus ( a nin Z or not a nin dom f ) by A9; :: thesis: verum

end;

defpred S₃[ set , set ] means ex n being Nat st
( $2 = (iter (f,n)) . $1 & $2 nin A & ( for i being Nat st i < n holds
(iter (f,i)) . $1 in A ) );
A11: for a being set st a in (dom f) \ Z holds
ex b being set st S₃[a,b]

proof

let a be set ; :: thesis: ( a in (dom f) \ Z implies ex b being set st S₃[a,b] )
assume A12: a in (dom f) \ Z ; :: thesis: ex b being set st S₃[a,b]
then a nin Z by XBOOLE_0:def 5;
then not f orbit a c= A by A9, A12;
then consider y being set such that
A13: y in f orbit a and
A14: y nin A by TARSKI:def 3;
A15: ex n1 being Element of NAT st
( y = (iter (f,n1)) . a & a in dom (iter (f,n1)) ) by A13;
defpred S₄[ Nat] means (iter (f,$1)) . a nin A;
A16: ex n being Nat st S₄[n] by A14, A15;
consider n being Nat such that
A17: S₄[n] and
A18: for m being Nat st S₄[m] holds
n <= m from NAT_1:sch 5(A16);
take b = (iter (f,n)) . a; :: thesis: S₃[a,b]
take n ; :: thesis: ( b = (iter (f,n)) . a & b nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) )
thus ( b = (iter (f,n)) . a & b nin A ) by A17; :: thesis: for i being Nat st i < n holds
(iter (f,i)) . a in A
let i be Nat; :: thesis: ( i < n implies (iter (f,i)) . a in A )
thus ( i < n implies (iter (f,i)) . a in A ) by A18; :: thesis: verum

end;

consider h being Function such that
A19: dom h = (dom f) \ Z and
A20: for a being set st a in (dom f) \ Z holds
S₃[a,h . a] from CLASSES1:sch 1(A11);
take g = (Z --> x) +* h; :: thesis: ( dom g = dom f & ( for a being set st a in dom f holds
( ( f orbit a c= A implies g . 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
g . a = (iter (f,n)) . a ) ) ) )
dom (Z --> x) = Z by FUNCOP_1:13;
hence dom g = Z \/ ((dom f) \ Z) by A19, FUNCT_4:def 1
.= dom f by A10, XBOOLE_1:45 ;
:: thesis: for a being set st a in dom f holds
( ( f orbit a c= A implies g . 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
g . a = (iter (f,n)) . a ) )
let a be set ; :: thesis: ( a in dom f implies ( ( f orbit a c= A implies g . 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
g . a = (iter (f,n)) . a ) ) )
assume A21: a in dom f ; :: thesis: ( ( f orbit a c= A implies g . 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
g . a = (iter (f,n)) . a ) )

hereby :: thesis: 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
g . a = (iter (f,n)) . a

assume f orbit a c= A ; :: thesis: g . a = x
then A22: a in Z by A9, A21;
then A23: a nin (dom f) \ Z by XBOOLE_0:def 5;
(Z --> x) . a = x by A22, FUNCOP_1:7;
hence g . a = x by A19, A23, FUNCT_4:11; :: thesis: verum

end;

let n be Nat; :: thesis: ( (iter (f,n)) . a nin A & ( for i being Nat st i < n holds
(iter (f,i)) . a in A ) implies g . a = (iter (f,n)) . a )
assume that
A24: (iter (f,n)) . a nin A and
A25: for i being Nat st i < n holds
(iter (f,i)) . a in A ; :: thesis: g . a = (iter (f,n)) . a
A26: n in NAT by ORDINAL1:def 12;
then a in dom (iter (f,n)) by A8, A21;
then (iter (f,n)) . a in f orbit a by A26;
then not f orbit a c= A by A24;
then a nin Z by A9;
then A27: a in (dom f) \ Z by A21, XBOOLE_0:def 5;
then consider n2 being Nat such that
A28: h . a = (iter (f,n2)) . a and
A29: h . a nin A and
A30: for i being Nat st i < n2 holds
(iter (f,i)) . a in A by A20;
A31: n <= n2 by A25, A28, A29;
n2 <= n by A24, A30;
then n = n2 by A31, XXREAL_0:1;
hence g . a = (iter (f,n)) . a by A19, A27, A28, FUNCT_4:13; :: thesis: verum