A7: dom F₃() = omega by FUNCT_2:def 1;
A8: F₂() in rng F₃() by A5, A7, FUNCT_1:def 3;
hence F₂() c= Union F₃() by ZFMISC_1:74; :: thesis: ( F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )
set phi = F₃();

A9: now :: thesis: for a being Ordinal holds not S₁[a]

defpred S₁[ Ordinal] means ( $1 in F₁() & $1 c/= F₄($1) );
assume A10: ex a being Ordinal st S₁[a] ; :: thesis: contradiction
consider a being Ordinal such that
A11: S₁[a] and
A12: for b being Ordinal st S₁[b] holds
a c= b from ORDINAL1:sch 1(A10);
F₄(F₄(a)) in F₄(a) by A3, A11, ORDINAL1:16;
then F₄(a) c/= F₄(F₄(a)) by ORDINAL1:5;
hence contradiction by A2, A11, A12; :: thesis: verum

end;

then F₂() c= F₄(F₂()) ;
then A13: ( F₂() c< F₄(F₂()) or F₂() = F₄(F₂()) ) ;

per cases ( F₄(F₂()) = F₂() or F₂() in F₄(F₂()) ) by A13, ORDINAL1:11;

suppose A14: F₄(F₂()) = F₂() ; :: thesis: ( F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

A15: for a being set st a in omega holds
F₃() . a = F₂()

proof

let a be set ; :: thesis: ( a in omega implies F₃() . a = F₂() )
assume a in omega ; :: thesis: F₃() . a = F₂()
then reconsider a = a as Element of omega ;
defpred S₁[ Nat] means F₃() . $1 = F₂();
A16: S₁[ 0 ] by A5;

A17: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A18: S₁[n] ; :: thesis: S₁[n + 1]
A19: Segm (n + 1) = succ (Segm n) by NAT_1:38;
n in omega by ORDINAL1:def 12;
then F₃() . (succ n) = F₄(F₂()) by A6, A18;
hence S₁[n + 1] by A14, A19; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A16, A17);
then S₁[a] ;
hence F₃() . a = F₂() ; :: thesis: verum

end;

rng F₃() = {F₂()}

proof

thus rng F₃() c= {F₂()} :: according to XBOOLE_0:def 10 :: thesis: {F₂()} c= rng F₃()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F₃() or x in {F₂()} )
assume x in rng F₃() ; :: thesis: x in {F₂()}
then consider a being object such that
A20: ( a in dom F₃() & x = F₃() . a ) by FUNCT_1:def 3;
x = F₂() by A15, A20, A7;
hence x in {F₂()} by TARSKI:def 1; :: thesis: verum

end;

thus {F₂()} c= rng F₃() by A8, ZFMISC_1:31; :: thesis: verum

end;

then Union F₃() = F₂() by ZFMISC_1:25;
hence ( F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) ) by A14; :: thesis: verum

end;

suppose A21: F₂() in F₄(F₂()) ; :: thesis: ( F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

deffunc H₁( Ordinal, Ordinal) -> Ordinal = F₄($2);
deffunc H₂( Ordinal, Sequence) -> set = {} ;

A22: now :: thesis: for a being Ordinal st succ a in omega holds
F₃() . (succ a) = H₁(a,F₃() . a)

let a be Ordinal; :: thesis: ( succ a in omega implies F₃() . (succ a) = H₁(a,F₃() . a) )
assume A23: succ a in omega ; :: thesis: F₃() . (succ a) = H₁(a,F₃() . a)
a in succ a by ORDINAL1:6;
hence F₃() . (succ a) = H₁(a,F₃() . a) by A6, A23, ORDINAL1:10; :: thesis: verum

end;

A24: for a being Ordinal st a in omega holds
( F₂() c= F₃() . a & F₃() . a in F₃() . (succ a) )

proof

let a be Ordinal; :: thesis: ( a in omega implies ( F₂() c= F₃() . a & F₃() . a in F₃() . (succ a) ) )
assume a in omega ; :: thesis: ( F₂() c= F₃() . a & F₃() . a in F₃() . (succ a) )
then reconsider a = a as Element of omega ;
defpred S₁[ Nat] means ( F₂() c= F₃() . $1 & F₃() . $1 in F₃() . (succ (Segm $1)) );
A25: S₁[ 0 ] by A21, A5, A6;

A26: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A27: S₁[n] ; :: thesis: S₁[n + 1]
A28: ( Segm (n + 1) = succ (Segm n) & Segm ((n + 1) + 1) = succ (Segm (n + 1)) & n + 1 in omega & (n + 1) + 1 in omega ) by NAT_1:38;
then ( F₃() . (n + 1) = F₄((F₃() . n)) & F₃() . ((n + 1) + 1) = F₄((F₃() . (n + 1))) ) by A22;
then ( F₃() . n c= F₃() . (n + 1) & F₃() . (n + 1) in F₃() . ((n + 1) + 1) ) by A3, A9, A27, A28;
hence S₁[n + 1] by A27, XBOOLE_1:1, A28; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A26);
then S₁[a] ;
hence ( F₂() c= F₃() . a & F₃() . a in F₃() . (succ a) ) ; :: thesis: verum

end;

deffunc H₃( Ordinal) -> Ordinal = F₄($1);
consider fi being Ordinal-Sequence such that
A29: ( dom fi = Union F₃() & ( for a being Ordinal st a in Union F₃() holds
fi . a = H₃(a) ) ) from ORDINAL2:sch 3();
1 = succ 0 ;
then F₃() . 1 = H₃(F₂()) by A5, A6;
then H₃(F₂()) in rng F₃() by A7, FUNCT_1:def 3;
then A30: H₃(F₂()) c= Union F₃() by ZFMISC_1:74;
A31: Union F₃() in F₁() by A1, Th41;

now :: thesis: for c being Ordinal st c in Union F₃() holds
succ c in Union F₃()

let c be Ordinal; :: thesis: ( c in Union F₃() implies succ c in Union F₃() )
assume c in Union F₃() ; :: thesis: succ c in Union F₃()
then consider x being object such that
A32: ( x in dom F₃() & c in F₃() . x ) by CARD_5:2;
reconsider x = x as Element of omega by A32, FUNCT_2:def 1;
( succ c c= F₃() . x & F₃() . x in F₃() . (succ x) ) by A24, A32, ORDINAL1:21;
then ( succ c in F₃() . (succ x) & succ x in omega ) by ORDINAL1:12, ORDINAL1:def 12;
hence succ c in Union F₃() by A7, CARD_5:2; :: thesis: verum

end;

then A33: Union F₃() is limit_ordinal by ORDINAL1:28;
then A34: H₃( Union F₃()) is_limes_of fi by A4, A21, A29, A30, A31;
fi is increasing

proof

let a be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in dom fi or fi . a in fi . b₁ )
let b be Ordinal; :: thesis: ( not a in b or not b in dom fi or fi . a in fi . b )
assume A35: ( a in b & b in dom fi ) ; :: thesis: fi . a in fi . b
then ( fi . a = H₃(a) & fi . b = H₃(b) & b in F₁() ) by A31, A29, ORDINAL1:10;
hence fi . a in fi . b by A3, A35; :: thesis: verum

end;

then A36: sup fi = lim fi by A21, A29, A30, A33, ORDINAL4:8
.= H₃( Union F₃()) by A34, ORDINAL2:def 10 ;
thus H₃( Union F₃()) c= Union F₃() :: according to XBOOLE_0:def 10 :: thesis: ( Union F₃() c= F₄((Union F₃())) & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in H₃( Union F₃()) or x in Union F₃() )
assume A37: x in H₃( Union F₃()) ; :: thesis: x in Union F₃()
reconsider A = x as Ordinal ;
consider b being Ordinal such that
A38: ( b in rng fi & A c= b ) by A36, A37, ORDINAL2:21;
consider y being object such that
A39: ( y in dom fi & b = fi . y ) by A38, FUNCT_1:def 3;
reconsider y = y as Ordinal by A39;
consider z being object such that
A40: ( z in dom F₃() & y in F₃() . z ) by A29, A39, CARD_5:2;
reconsider z = z as Ordinal by A40;
set c = F₃() . z;
succ z in omega by A7, A40, ORDINAL1:28;
then A41: ( F₃() . (succ z) = H₃(F₃() . z) & F₃() . (succ z) in rng F₃() & b = H₃(y) ) by A7, A22, A29, A39, FUNCT_1:def 3;
( b in H₃(F₃() . z) & H₃(F₃() . z) c= Union F₃() ) by A41, A3, A40, ZFMISC_1:74;
hence x in Union F₃() by A38, ORDINAL1:12; :: thesis: verum

end;

thus Union F₃() c= H₃( Union F₃()) by A9, A1, Th41; :: thesis: for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b
let b be Ordinal; :: thesis: ( F₂() c= b & b in F₁() & F₄(b) = b implies Union F₃() c= b )
assume A42: ( F₂() c= b & b in F₁() & H₃(b) = b ) ; :: thesis: Union F₃() c= b
rng F₃() c= b

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng F₃() or x in b )
assume x in rng F₃() ; :: thesis: x in b
then consider a being object such that
A43: ( a in dom F₃() & x = F₃() . a ) by FUNCT_1:def 3;
reconsider a = a as Element of omega by A43, FUNCT_2:def 1;
defpred S₁[ Nat] means F₃() . $1 in b;
F₂() <> b by A21, A42;
then F₂() c< b by A42;
then A44: S₁[ 0 ] by A5, ORDINAL1:11;

A45: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then ( H₃(F₃() . n) in b & n in omega ) by A3, A42, ORDINAL1:def 12;
then A46: F₃() . (succ n) in b by A6;
Segm (n + 1) = succ (Segm n) by NAT_1:38;
hence S₁[n + 1] by A46; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A44, A45);
then S₁[a] ;
hence x in b by A43; :: thesis: verum

end;

then ( Union F₃() c= union b & union b c= b ) by ORDINAL2:5, ZFMISC_1:77;
hence Union F₃() c= b ; :: thesis: verum

end;

end;