assume A3: 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, T-Sequence) -> set = {} ;
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: ( {} in omega implies phi . {} = succ F₂() ) and
A6: for a being ordinal number st succ a in omega holds
phi . (succ a) = H₁(a,phi . a) and
for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
phi . a = H₂(a,phi | a) from ORDINAL2:sch 11();
K0: rng phi c= On F₁()

proof

let y be set ; :: 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 set such that
K1: ( x in dom phi & y = phi . x ) by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A4, K1;
defpred S₁[ Nat] means phi . $1 in On F₁();
K2: S₁[ 0 ] by A5, ORDINAL1:def 9;
K3: 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 K5: phi . n in F₁() by ORDINAL1:def 9;
K4: n + 1 = succ n by NAT_1:38;
( phi . (n + 1) = F₃((phi . n)) & F₃((phi . n)) in F₁() ) by A6, K4, K5, P0;
hence S₁[n + 1] by ORDINAL1:def 9; :: thesis: verum

end;

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

end;

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

A7: now

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

end;

A11: now

let a be ordinal number ; :: 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 A3, A7;
then a c< F₃(a) by XBOOLE_0:def 8;
hence a in F₃(a) by ORDINAL1:11; :: thesis: verum

end;

B1: for a being ordinal number st a in omega holds
F₂() in phi . a

proof

let a be ordinal number ; :: 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;
B01: S₁[ 0 ] by A5, ORDINAL1:6;

B02: now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B03: S₁[n] ; :: thesis: S₁[n + 1]
( n + 1 = succ 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 B03, A11;
hence S₁[n + 1] by B03, ORDINAL1:10; :: thesis: verum

end;

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

end;

A12: phi is increasing

proof

let a be ordinal number ; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 phi or phi . a in phi . b₁ )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 phi or phi . a in phi . b )
assume A13: ( a in b & b in dom phi ) ; :: thesis: phi . a in phi . b
then A14: ex c being ordinal number st
( b = a +^ c & c <> {} ) by ORDINAL3:28;
defpred S₁[ Ordinal] means ( a +^ $1 in omega & $1 <> {} implies phi . a in phi . (a +^ $1) );
A15: S₁[ {} ] ;
A16: for c being ordinal number st S₁[c] holds
S₁[ succ c]

proof

let c be ordinal number ; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume that
A17: ( a +^ c in omega & c <> {} implies phi . a in phi . (a +^ c) ) and
A18: ( a +^ (succ c) in omega & succ c <> {} ) ; :: thesis: phi . a in phi . (a +^ (succ c))
A19: ( 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 A18, A19, ORDINAL1:10;
then ( phi . (a +^ (succ c)) = F₃(d) & d in F₃(d) & a +^ {} = a ) by A6, A11, A18, A19, B1, ORDINAL2:27;
hence phi . a in phi . (a +^ (succ c)) by A17, A18, A19, ORDINAL1:10; :: thesis: verum

end;

A20: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S₁[c] ) holds
S₁[b]

proof

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

end;

for c being ordinal number holds S₁[c] from ORDINAL2:sch 1(A15, A16, A20);
hence phi . a in phi . b by A4, A13, A14; :: thesis: verum

end;

J1: sup phi in F₁() by A0, ThC2;
deffunc H₃( Ordinal) -> Ordinal = F₃($1);
consider fi being Ordinal-Sequence such that
A23: ( dom fi = sup phi & ( for a being ordinal number 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, Lm1, FUNCT_1:def 3;
then A24: ( sup phi <> {} & sup phi is limit_ordinal ) by A4, A12, ORDINAL2:19, ORDINAL4:16;
then A25: H₃( sup phi) is_limes_of fi by J1, A2, A23;
fi is increasing

proof

let a be ordinal number ; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 fi or fi . a in fi . b₁ )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 fi or fi . a in fi . b )
assume A26: ( 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 J1, A23, ORDINAL1:10;
hence fi . a in fi . b by A1, A26; :: thesis: verum

end;

then A27: sup fi = lim fi by A23, A24, ORDINAL4:8
.= H₃( sup phi) by A25, ORDINAL2:def 10 ;
ZZ: 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 A28: x in sup fi ; :: thesis: x in sup phi
reconsider A = x as Ordinal ;
consider b being ordinal number such that
A29: ( b in rng fi & A c= b ) by A28, ORDINAL2:21;
consider y being set such that
A30: ( y in dom fi & b = fi . y ) by A29, FUNCT_1:def 3;
reconsider y = y as Ordinal by A30;
consider c being ordinal number such that
A31: ( c in rng phi & y c= c ) by A23, A30, ORDINAL2:21;
C1: c in F₁() by K0, A31, ORDINAL1:def 9;
consider z being set such that
A32: ( z in dom phi & c = phi . z ) by A31, FUNCT_1:def 3;
reconsider z = z as Ordinal by A32;
succ z in omega by A4, A32, ORDINAL1:28;
then A33: ( phi . (succ z) = H₃(c) & phi . (succ z) in rng phi & b = H₃(y) ) by A4, A6, A23, A30, A32, FUNCT_1:def 3;
( y c< c iff ( y <> c & y c= c ) ) by XBOOLE_0:def 8;
then ( H₃(y) in H₃(c) or y = c ) by C1, A1, A31, ORDINAL1:11;
then ( b c= H₃(c) & H₃(c) in sup phi ) by A33, ORDINAL1:def 2, ORDINAL2:19;
then b in sup phi by ORDINAL1:12;
hence x in sup phi by A29, 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 B1, ORDINAL2:19;
then F₂() in sup phi by ORDINAL1:10;
hence contradiction by J1, A11, A27, ZZ, ORDINAL1:5; :: thesis: verum