assume A3: for a being Ordinal 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
A4: dom phi = omega and
A5: ( 0 in omega implies phi . 0 = succ F₁() ) and
A6: 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();

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

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

end;

A11: now :: thesis: for a being Ordinal st F₁() in a holds
a in F₂(a)

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

end;

A12: 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;
A13: S₁[ 0 ] by A5, ORDINAL1:6;

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

end;

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

end;

A16: 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 A17: ( a in b & b in dom phi ) ; :: thesis: phi . a in phi . b
then A18: 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) );
A19: S₁[ 0 ] ;
A20: 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
A21: ( a +^ c in omega & c <> {} implies phi . a in phi . (a +^ c) ) and
A22: ( a +^ (succ c) in omega & succ c <> {} ) ; :: thesis: phi . a in phi . (a +^ (succ c))
A23: ( 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 A22, A23, ORDINAL1:10;
then ( phi . (a +^ (succ c)) = F₂(d) & d in F₂(d) & a +^ {} = a ) by A6, A11, A22, A23, A12, ORDINAL2:27;
hence phi . a in phi . (a +^ (succ c)) by A21, A22, A23, ORDINAL1:10; :: thesis: verum

end;

A24: 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
A25: ( 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
A26: ( a +^ b in omega & b <> {} ) ; :: thesis: phi . a in phi . (a +^ b)
a +^ b <> {} by A26, ORDINAL3:26;
then ( a +^ b is limit_ordinal & {} in a +^ b ) by A25, ORDINAL3:8, ORDINAL3:29;
hence phi . a in phi . (a +^ b) by A26; :: thesis: verum

end;

for c being Ordinal holds S₁[c] from ORDINAL2:sch 1(A19, A20, A24);
hence phi . a in phi . b by A4, A17, A18; :: thesis: verum

end;

deffunc H₃( Ordinal) -> Ordinal = F₂($1);
consider fi being Ordinal-Sequence such that
A27: ( 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 A4, A5, FUNCT_1:def 3;
then A28: ( sup phi <> {} & sup phi is limit_ordinal ) by A4, A16, ORDINAL2:19, ORDINAL4:16;
then A29: H₃( sup phi) is_limes_of fi by A2, A27;
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 A30: ( a in b & b in dom fi ) ; :: thesis: fi . a in fi . b
then ( fi . a = H₃(a) & fi . b = H₃(b) ) by A27, ORDINAL1:10;
hence fi . a in fi . b by A1, A30; :: thesis: verum

end;

then A31: sup fi = lim fi by A27, A28, ORDINAL4:8
.= H₃( sup phi) by A29, ORDINAL2:def 10 ;
A32: 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 A33: x in sup fi ; :: thesis: x in sup phi
reconsider A = x as Ordinal ;
consider b being Ordinal such that
A34: ( b in rng fi & A c= b ) by 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 c being Ordinal such that
A36: ( c in rng phi & y c= c ) by A27, A35, ORDINAL2:21;
consider z being object such that
A37: ( z in dom phi & c = phi . z ) by A36, FUNCT_1:def 3;
reconsider z = z as Ordinal by A37;
succ z in omega by A4, A37, ORDINAL1:28;
then A38: ( phi . (succ z) = H₃(c) & phi . (succ z) in rng phi & b = H₃(y) ) by A4, A6, A27, A35, A37, FUNCT_1:def 3;
( y c< c iff ( y <> c & y c= c ) ) ;
then ( H₃(y) in H₃(c) or y = c ) by A1, A36, ORDINAL1:11;
then ( b c= H₃(c) & H₃(c) in sup phi ) by A38, ORDINAL1:def 2, ORDINAL2:19;
then b in sup phi by ORDINAL1:12;
hence x in sup phi by A34, ORDINAL1:12; :: thesis: verum

end;

phi . 0 in rng phi by A4, FUNCT_1:def 3;
then ( F₁() in phi . 0 & phi . 0 in sup phi ) by A12, ORDINAL2:19;
then F₁() in sup phi by ORDINAL1:10;
hence contradiction by A11, A31, A32, ORDINAL1:5; :: thesis: verum