A5: F₁() in rng F₂() by A3, 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 & F₃(b) = b holds
Union F₂() c= b ) )
set phi = F₂();

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

defpred S₁[ Ordinal] means not $1 c= F₃($1);
assume A7: ex a being Ordinal st S₁[a] ; :: thesis: contradiction
consider a being Ordinal such that
A8: S₁[a] and
A9: for b being Ordinal st S₁[b] holds
a c= b from ORDINAL1:sch 1(A7);
F₃(F₃(a)) in F₃(a) by A1, A8, ORDINAL1:16;
then not F₃(a) c= F₃(F₃(a)) by ORDINAL1:5;
hence contradiction by A8, A9; :: thesis: verum

end;

then F₁() c= F₃(F₁()) ;
then A10: ( F₁() c< F₃(F₁()) or F₁() = F₃(F₁()) ) ;

per cases ( F₃(F₁()) = F₁() or F₁() in F₃(F₁()) ) by A10, ORDINAL1:11;

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

A12: 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₁();
A13: S₁[ 0 ] by A3;

A14: 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 A15: S₁[n] ; :: thesis: S₁[n + 1]
A16: Segm (n + 1) = succ (Segm n) by NAT_1:38;
n in omega by ORDINAL1:def 12;
then F₂() . (succ n) = F₃(F₁()) by A4, A15;
hence S₁[n + 1] by A11, A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A14);
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: not {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
A17: ( a in dom F₂() & x = F₂() . a ) by FUNCT_1:def 3;
x = F₁() by A12, A17, A3;
hence x in {F₁()} by TARSKI:def 1; :: thesis: verum

end;

thus not {F₁()} c/= rng F₂() by A5, 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 & F₃(b) = b holds
Union F₂() c= b ) ) by A11; :: thesis: verum

end;

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

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

A19: 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 A20: 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 A4, A20, ORDINAL1:10; :: thesis: verum

end;

A21: 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 $1) );
A22: S₁[ 0 ] by A18, A3, A4;

A23: 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 A24: S₁[n] ; :: thesis: S₁[n + 1]
A25: ( 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 A19;
then ( F₂() . n c= F₂() . (n + 1) & F₂() . (n + 1) in F₂() . ((n + 1) + 1) ) by A1, A6, A24, A25;
hence S₁[n + 1] by A24, XBOOLE_1:1, A25; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A22, A23);
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
A26: ( 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 A3, A4;
then H₃(F₁()) in rng F₂() by A3, FUNCT_1:def 3;
then A27: H₃(F₁()) c= Union F₂() by ZFMISC_1:74;

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
A28: ( x in dom F₂() & c in F₂() . x ) by CARD_5:2;
reconsider x = x as Element of omega by A3, A28;
( succ c c= F₂() . x & F₂() . x in F₂() . (succ x) ) by A21, A28, 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 A3, CARD_5:2; :: thesis: verum

end;

then A29: Union F₂() is limit_ordinal by ORDINAL1:28;
then A30: H₃( Union F₂()) is_limes_of fi by A2, A26, A27, A18;
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 A31: ( a in b & b in dom fi ) ; :: thesis: fi . a in fi . b
then ( fi . a = H₃(a) & fi . b = H₃(b) ) by A26, ORDINAL1:10;
hence fi . a in fi . b by A1, A31; :: thesis: verum

end;

then A32: sup fi = lim fi by A26, A27, A29, A18, ORDINAL4:8
.= H₃( Union F₂()) by A30, ORDINAL2:def 10 ;
thus H₃( Union F₂()) c= Union F₂() :: according to XBOOLE_0:def 10 :: thesis: ( not Union F₂() c/= F₃((Union F₂())) & ( for b being Ordinal st F₁() c= b & 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 A33: x in H₃( Union F₂()) ; :: thesis: x in Union F₂()
reconsider A = x as Ordinal ;
consider b being Ordinal such that
A34: ( b in rng fi & A c= b ) by A32, A33, ORDINAL2:21;
consider y being object such that
A35: ( y in dom fi & b = fi . y ) by A34, FUNCT_1:def 3;
reconsider y = y as Ordinal by A35;
consider z being object such that
A36: ( z in dom F₂() & y in F₂() . z ) by A26, A35, CARD_5:2;
reconsider z = z as Ordinal by A36;
set c = F₂() . z;
succ z in omega by A3, A36, ORDINAL1:28;
then ( F₂() . (succ z) = H₃(F₂() . z) & F₂() . (succ z) in rng F₂() & b = H₃(y) ) by A3, A19, A26, A35, FUNCT_1:def 3;
then ( b in H₃(F₂() . z) & H₃(F₂() . z) c= Union F₂() ) by A1, A36, ZFMISC_1:74;
hence x in Union F₂() by A34, ORDINAL1:12; :: thesis: verum

end;

thus Union F₂() c= H₃( Union F₂()) by A6; :: thesis: for b being Ordinal st F₁() c= b & F₃(b) = b holds
Union F₂() c= b
let b be Ordinal; :: thesis: ( F₁() c= b & F₃(b) = b implies Union F₂() c= b )
assume A37: ( F₁() c= b & 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
A38: ( a in dom F₂() & x = F₂() . a ) by FUNCT_1:def 3;
reconsider a = a as Element of omega by A3, A38;
defpred S₁[ Nat] means F₂() . $1 in b;
F₁() <> b by A18, A37;
then F₁() c< b by A37;
then A39: S₁[ 0 ] by A3, ORDINAL1:11;

A40: 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 A1, A37, ORDINAL1:def 12;
then A41: F₂() . (succ n) in b by A4;
Segm (n + 1) = succ (Segm n) by NAT_1:38;
hence S₁[n + 1] by A41; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A39, A40);
then S₁[a] ;
hence x in b by A38; :: 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;