assume A5: for a being Ordinal of F₁() holds
( not F₂() in a or not F₃(a) = a ) ; :: thesis: contradiction
deffunc H₁( Ordinal, Ordinal) -> Ordinal = F₃($2);
deffunc H₂( Ordinal, Sequence) -> set = {} ;
consider phi being Ordinal-Sequence such that
A6: dom phi = omega and
A7: ( 0 in omega implies phi . 0 = succ F₂() ) and
A8: for a being Ordinal st succ a in omega holds
phi . (succ a) = H₁(a,phi . a) and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
phi . a = H₂(a,phi | a) from ORDINAL2:sch 11();
A9: rng phi c= On F₁()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng phi or y in On F₁() )
assume y in rng phi ; :: thesis: y in On F₁()
then consider x being object such that
A10: ( x in dom phi & y = phi . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A6, A10;
defpred S₁[ Nat] means phi . $1 in On F₁();
A11: S₁[ 0 ] by A7, ORDINAL1:def 9;
A12: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then A13: phi . n in F₁() by ORDINAL1:def 9;
A14: Segm (n + 1) = succ (Segm n) by NAT_1:38;
( phi . (n + 1) = F₃((phi . n)) & F₃((phi . n)) in F₁() ) by A8, A14, A13, A2;
hence S₁[n + 1] by ORDINAL1:def 9; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A11, A12);
then S₁[x] ;
hence y in On F₁() by A10; :: thesis: verum

end;

then reconsider phi = phi as Ordinal-Sequence of omega,F₁() by A6, FUNCT_2:2;

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

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

end;

A19: now :: thesis: for a being Ordinal st F₂() in a & a in F₁() holds
a in F₃(a)

let a be Ordinal; :: thesis: ( F₂() in a & a in F₁() implies a in F₃(a) )
assume ( F₂() in a & a in F₁() ) ; :: thesis: a in F₃(a)
then ( a c= F₃(a) & a <> F₃(a) ) by A5, A15;
then a c< F₃(a) ;
hence a in F₃(a) by ORDINAL1:11; :: thesis: verum

end;

A20: for a being Ordinal st a in omega holds
F₂() in phi . a

proof

let a be Ordinal; :: thesis: ( a in omega implies F₂() in phi . a )
assume a in omega ; :: thesis: F₂() in phi . a
then reconsider a = a as Element of omega ;
defpred S₁[ Nat] means F₂() in phi . $1;
A21: S₁[ 0 ] by A7, ORDINAL1:6;

A22: 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 A23: S₁[n] ; :: thesis: S₁[n + 1]
( Segm (n + 1) = succ (Segm n) & n + 1 in omega ) by NAT_1:38;
then phi . (n + 1) = F₃((phi . n)) by A8;
then phi . n in phi . (n + 1) by A23, A19;
hence S₁[n + 1] by A23, ORDINAL1:10; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A21, A22);
then S₁[a] ;
hence F₂() in phi . a ; :: thesis: verum

end;

A24: phi 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 phi or phi . a in phi . b₁ )
let b be Ordinal; :: thesis: ( not a in b or not b in dom phi or phi . a in phi . b )
assume A25: ( a in b & b in dom phi ) ; :: thesis: phi . a in phi . b
then A26: ex c being Ordinal st
( b = a +^ c & c <> {} ) by ORDINAL3:28;
defpred S₁[ Ordinal] means ( a +^ $1 in omega & $1 <> {} implies phi . a in phi . (a +^ $1) );
A27: S₁[ 0 ] ;
A28: for c being Ordinal st S₁[c] holds
S₁[ succ c]

proof

let c be Ordinal; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume that
A29: ( a +^ c in omega & c <> {} implies phi . a in phi . (a +^ c) ) and
A30: ( a +^ (succ c) in omega & succ c <> {} ) ; :: thesis: phi . a in phi . (a +^ (succ c))
A31: ( a +^ c in succ (a +^ c) & a +^ (succ c) = succ (a +^ c) ) by ORDINAL1:6, ORDINAL2:28;
reconsider d = phi . (a +^ c) as Ordinal ;
a +^ c in omega by A30, A31, ORDINAL1:10;
then ( phi . (a +^ (succ c)) = F₃(d) & d in F₃(d) & a +^ {} = a ) by A8, A19, A30, A31, A20, ORDINAL2:27;
hence phi . a in phi . (a +^ (succ c)) by A29, A30, A31, ORDINAL1:10; :: thesis: verum

end;

A32: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

proof

let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) implies S₁[b] )
assume that
A33: ( b <> 0 & b is limit_ordinal ) and
for c being Ordinal st c in b & a +^ c in omega & c <> {} holds
phi . a in phi . (a +^ c) and
A34: ( a +^ b in omega & b <> {} ) ; :: thesis: phi . a in phi . (a +^ b)
( a +^ b is limit_ordinal & {} in a +^ b ) by A33, ORDINAL3:8, ORDINAL3:29;
hence phi . a in phi . (a +^ b) by A34; :: thesis: verum

end;

for c being Ordinal holds S₁[c] from ORDINAL2:sch 1(A27, A28, A32);
hence phi . a in phi . b by A6, A25, A26; :: thesis: verum

end;

A35: sup phi in F₁() by A1, Th42;
deffunc H₃( Ordinal) -> Ordinal = F₃($1);
consider fi being Ordinal-Sequence such that
A36: ( dom fi = sup phi & ( for a being Ordinal st a in sup phi holds
fi . a = H₃(a) ) ) from ORDINAL2:sch 3();
( succ F₂() in rng phi & sup (rng phi) = sup phi ) by A6, A7, FUNCT_1:def 3;
then A37: ( sup phi <> {} & sup phi is limit_ordinal ) by A6, A24, ORDINAL2:19, ORDINAL4:16;
then A38: H₃( sup phi) is_limes_of fi by A35, A4, A36;
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 A39: ( 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 A35, A36, ORDINAL1:10;
hence fi . a in fi . b by A3, A39; :: thesis: verum

end;

then A40: sup fi = lim fi by A36, A37, ORDINAL4:8
.= H₃( sup phi) by A38, ORDINAL2:def 10 ;
A41: sup fi c= sup phi

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in sup fi or x in sup phi )
assume A42: x in sup fi ; :: thesis: x in sup phi
reconsider A = x as Ordinal ;
consider b being Ordinal such that
A43: ( b in rng fi & A c= b ) by A42, ORDINAL2:21;
consider y being object such that
A44: ( y in dom fi & b = fi . y ) by A43, FUNCT_1:def 3;
reconsider y = y as Ordinal by A44;
consider c being Ordinal such that
A45: ( c in rng phi & y c= c ) by A36, A44, ORDINAL2:21;
A46: c in F₁() by A9, A45, ORDINAL1:def 9;
consider z being object such that
A47: ( z in dom phi & c = phi . z ) by A45, FUNCT_1:def 3;
reconsider z = z as Ordinal by A47;
succ z in omega by A6, A47, ORDINAL1:28;
then A48: ( phi . (succ z) = H₃(c) & phi . (succ z) in rng phi & b = H₃(y) ) by A6, A8, A36, A44, A47, FUNCT_1:def 3;
( y c< c iff ( y <> c & y c= c ) ) ;
then ( H₃(y) in H₃(c) or y = c ) by A46, A3, A45, ORDINAL1:11;
then ( b c= H₃(c) & H₃(c) in sup phi ) by A48, ORDINAL1:def 2, ORDINAL2:19;
then b in sup phi by ORDINAL1:12;
hence x in sup phi by A43, ORDINAL1:12; :: thesis: verum

end;

phi . 0 in rng phi by A6, FUNCT_1:def 3;
then ( F₂() in phi . 0 & phi . 0 in sup phi ) by A20, ORDINAL2:19;
then F₂() in sup phi by ORDINAL1:10;
hence contradiction by A35, A19, A40, A41, ORDINAL1:5; :: thesis: verum