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

end;

consider h being Function such that
A17: dom h = (dom f) \ Z and
A18: for a being set st a in (dom f) \ Z holds
S₃[a,h . a] from CLASSES1:sch 1(A11);
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:19;
then dom ((Z --> 0 ) +* (g | Z)) = Z \/ (dom (g | Z)) by FUNCT_4:def 1
.= Z by RELAT_1:87, XBOOLE_1:12 ;
hence dom i = Z \/ ((dom f) \ Z) by A17, 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 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 A19: 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 A20: a in Z by A19, A9;
then ( a nin (dom f) \ Z & (Z --> 0 ) . a = 0 ) by FUNCOP_1:13, XBOOLE_0:def 5;
then A21: i . a = ((Z --> 0 ) +* (g | Z)) . a by A17, FUNCT_4:12;

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 A21, FUNCT_4:14;
hence i . a = g . a by A20, FUNCT_1:72; :: thesis: verum

end;

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

then ( i . a = (Z --> 0 ) . a & (Z --> 0 ) . a = 0 & a nin dom g ) by A20, A21, FUNCOP_1:13, FUNCT_4:12, RELAT_1:86;
hence i . a = g . a by FUNCT_1:def 4; :: 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 n' = n as Element of NAT by ORDINAL1:def 13;
assume A22: ( (iter f,n) . a nin A & ( 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,n') by A19, A8;
then (iter f,n) . a in f orbit a ;
then not f orbit a c= A by A22;
then a nin Z by A9;
then A23: a in (dom f) \ Z by A19, XBOOLE_0:def 5;
then consider n2 being Nat such that
A24: ( h . a = (iter f,n2) . a & h . a nin A & ( for i being Nat st i < n2 holds
(iter f,i) . a in A ) ) by A18;
( n <= n2 & n2 <= n ) by A22, A24;
then n = n2 by XXREAL_0:1;
hence i . a = (iter f,n) . a by A17, A23, A24, FUNCT_4:14; :: thesis: verum