assume A3: for a being Ordinal holds
( not F1() in a or not F2(a) = a ) ; :: thesis: contradiction
deffunc H1( Ordinal, Ordinal) -> Ordinal = F2($2);
deffunc H2( Ordinal, Sequence) -> set = {} ;
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: ( 0 in omega implies phi . 0 = succ F1() ) and
A6: for a being Ordinal st succ a in omega holds
phi . (succ a) = H1(a,phi . a) and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
phi . a = H2(a,phi | a) from ORDINAL2:sch 11();
A7: now :: thesis: for a being Ordinal holds not S1[a]
defpred S1[ Ordinal] means not $1 c= F2($1);
assume A8: ex a being Ordinal st S1[a] ; :: thesis: contradiction
consider a being Ordinal such that
A9: S1[a] and
A10: for b being Ordinal st S1[b] holds
a c= b from ORDINAL1:sch 1(A8);
 F2(F2(a)) in F2(a) by A1, A9, ORDINAL1:16;
then not F2(a) c= F2(F2(a)) by ORDINAL1:5;
hence contradiction by A9, A10; :: thesis: verum
end;
A11: now :: thesis: for a being Ordinal st F1() in a holds
a in F2(a)
let a be Ordinal; :: thesis: ( F1() in a implies a in F2(a) )
assume F1() in a ; :: thesis: a in F2(a)
then ( a c= F2(a) & a <> F2(a) ) by A3, A7;
then a c< F2(a) ;
hence a in F2(a) by ORDINAL1:11; :: thesis: verum
end;
A12: for a being Ordinal st a in omega holds
F1() in phi . a
proof
let a be Ordinal; :: thesis: ( a in omega implies F1() in phi . a )
assume a in omega ; :: thesis: F1() in phi . a
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means F1() in phi . $1;
A13: S1[ 0 ] by A5, ORDINAL1:6;
A14: now :: thesis: for n being Nat st S1[n] holds
S1[n + 1]
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A15: S1[n] ; :: thesis: S1[n + 1]
( Segm (n + 1) = succ (Segm n) & n + 1 in omega ) by NAT_1:38;
then phi . (n + 1) = F2((phi . n)) by A6;
then phi . n in phi . (n + 1) by A15, A11;
hence S1[n + 1] by A15, ORDINAL1:10; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A13, A14);
 then S1[a] ;
hence F1() in phi . a ; :: thesis: verum
end;
A16: phi is increasing
proof
let a be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not a in b1 or not b1 in dom phi or phi . a in phi . b1 )
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 S1[ Ordinal] means ( a +^ $1 in omega & $1 <> {} implies phi . a in phi . (a +^ $1) );
A19: S1[ 0 ] ;
A20: for c being Ordinal st S1[c] holds
S1[ succ c]
proof
let c be Ordinal; :: thesis: ( S1[c] implies S1[ 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)) = F2(d) & d in F2(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
S1[c] ) holds
S1[b]
proof
let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S1[c] ) implies S1[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 S1[c] from ORDINAL2:sch 1(A19, A20, A24);
 hence phi . a in phi . b by A4, A17, A18; :: thesis: verum
end;
deffunc H3( Ordinal) -> Ordinal = F2($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 = H3(a) ) ) from ORDINAL2:sch 3();
 ( succ F1() 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: H3( sup phi) is_limes_of fi by A2, A27;
fi is increasing
proof
let a be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not a in b1 or not b1 in dom fi or fi . a in fi . b1 )
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 = H3(a) & fi . b = H3(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
.= H3( 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) = H3(c) & phi . (succ z) in rng phi & b = H3(y) ) by A4, A6, A27, A35, A37, FUNCT_1:def 3;
( y c< c iff ( y <> c & y c= c ) ) ;
then ( H3(y) in H3(c) or y = c ) by A1, A36, ORDINAL1:11;
then ( b c= H3(c) & H3(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 ( F1() in phi . 0 & phi . 0 in sup phi ) by A12, ORDINAL2:19;
then F1() in sup phi by ORDINAL1:10;
hence contradiction by A11, A31, A32, ORDINAL1:5; :: thesis: verum