defpred S₂[ object ] means f orbit $1 c= A;
consider Z being set such that
A10: for a being object holds
( a in Z iff ( a in dom f & S₂[a] ) ) from XBOOLE_0:sch 1();
A11: Z c= dom f by A10;
defpred S₃[ object , object ] 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 ) );
A12: for a being object st a in (dom f) \ Z holds
ex b being object st S₃[a,b]

proof

let a be object ; :: thesis: ( a in (dom f) \ Z implies ex b being object st S₃[a,b] )
assume A13: a in (dom f) \ Z ; :: thesis: ex b being object st S₃[a,b]
then a nin Z by XBOOLE_0:def 5;
then not f orbit a c= A by A10, A13;
then consider y being object such that
A14: y in f orbit a and
A15: y nin A ;
A16: ex n1 being Element of NAT st
( y = (iter (f,n1)) . a & a in dom (iter (f,n1)) ) by A14;
defpred S₄[ Nat] means (iter (f,$1)) . a nin A;
A17: ex n being Nat st S₄[n] by A15, A16;
consider n being Nat such that
A18: S₄[n] and
A19: for m being Nat st S₄[m] holds
n <= m from NAT_1:sch 5(A17);
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 A18; :: 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 A19; :: thesis: verum

end;

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

assume f orbit a c= A ; :: thesis: i . a = g . a
then A23: a in Z by A10, A22;
then a nin (dom f) \ Z by XBOOLE_0:def 5;
then A24: i . a = ((Z --> 0) +* (g | Z)) . a by A20, FUNCT_4:11;

per cases ( a in dom (g | Z) or a nin dom (g | Z) ) ;

suppose a in dom (g | Z) ; :: thesis: i . a = g . a

then i . a = (g | Z) . a by A24, FUNCT_4:13;
hence i . a = g . a by A23, FUNCT_1:49; :: thesis: verum

end;

suppose A25: a nin dom (g | Z) ; :: thesis: i . a = g . a

then A26: i . a = (Z --> 0) . a by A24, FUNCT_4:11;
A27: (Z --> 0) . a = 0 by A23, FUNCOP_1:7;
a nin dom g by A23, A25, RELAT_1:57;
hence i . a = g . a by A26, A27, FUNCT_1:def 2; :: thesis: verum

end;

end;

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 i . a = (iter (f,n)) . a )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume that
A28: (iter (f,n)) . a nin A and
A29: for i being Nat st i < n holds
(iter (f,i)) . a in A ; :: thesis: i . a = (iter (f,n)) . a
a in dom (iter (f,n9)) by A9, A22;
then (iter (f,n)) . a in f orbit a ;
then not f orbit a c= A by A28;
then a nin Z by A10;
then A30: a in (dom f) \ Z by A22, XBOOLE_0:def 5;
then consider n2 being Nat such that
A31: h . a = (iter (f,n2)) . a and
A32: h . a nin A and
A33: for i being Nat st i < n2 holds
(iter (f,i)) . a in A by A21;
A34: n <= n2 by A29, A31, A32;
n2 <= n by A28, A33;
then n = n2 by A34, XXREAL_0:1;
hence i . a = (iter (f,n)) . a by A20, A30, A31, FUNCT_4:13; :: thesis: verum