:: ORDINAL5 semantic presentation

begin


theorem Th1: :: ORDINAL5:1
for a, b being ordinal number holds
( not a c= succ b or a c= b or a = succ b )
proof
let a, b be ordinal number ; ::_thesis: ( not a c= succ b or a c= b or a = succ b )
assume A1: a c= succ b ; ::_thesis: ( a c= b or a = succ b )
assume  a c/= b ; ::_thesis: a = succ b
then A2: b in a by ORDINAL1:16;
thus  a c= succ b by A1; :: according to XBOOLE_0:def_10 ::_thesis: succ b c= a
thus  succ b c= a by A2, ORDINAL1:21; ::_thesis: verum
end;

registration
cluster NAT  ->  limit_ordinal ;
coherence
 omega is limit_ordinal ;
cluster empty  ->  empty Ordinal-yielding for set ;
coherence
 for b1 being empty set holds b1 is Ordinal-yielding
proof
let f be empty set ; ::_thesis: f is Ordinal-yielding
take  0 ; :: according to ORDINAL2:def_4 ::_thesis: rng f c= 0
thus  rng f c= 0 ; ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like non empty T-Sequence-like finite for set ;
existence
 ex b1 being T-Sequence st
( not b1 is empty & b1 is finite )
proof
set x = the set ;
take  <% the set %> ; ::_thesis: ( not <% the set %> is empty & <% the set %> is finite )
thus  ( not <% the set %> is empty & <% the set %> is finite ) ; ::_thesis: verum
end;
end;

registration
let f be T-Sequence;
let g be non empty T-Sequence;
clusterf ^ g ->  non empty ;
coherence
 not f ^ g is empty
proof
 (dom f) +^ (dom g) <> 0 by ORDINAL3:26;
then  dom (f ^ g) <> 0 by ORDINAL4:def_1;
hence  not f ^ g is empty ; ::_thesis: verum
end;
clusterg ^ f ->  non empty ;
coherence
 not g ^ f is empty
proof
 (dom g) +^ (dom f) <> 0 by ORDINAL3:26;
then  dom (g ^ f) <> 0 by ORDINAL4:def_1;
hence  not g ^ f is empty ; ::_thesis: verum
end;
end;


theorem Th2: :: ORDINAL5:2
for a, b being ordinal number
for S being T-Sequence st dom S = a +^ b holds
ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
proof
let a, b be ordinal number ; ::_thesis: for S being T-Sequence st dom S = a +^ b holds
ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
let S be T-Sequence; ::_thesis: ( dom S = a +^ b implies ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b ) )
assume A1: dom S = a +^ b ; ::_thesis: ex S1, S2 being T-Sequence st
( S = S1 ^ S2 & dom S1 = a & dom S2 = b )
set S1 = S | a;
B2: a c= a +^ b by ORDINAL3:24;
then A2: dom (S | a) = a by A1, RELAT_1:62;
deffunc H1( Ordinal) ->  set = S . (a +^ $1);
consider S2 being T-Sequence such that
A3: ( dom S2 = b & ( for c being ordinal number st c in b holds
S2 . c = H1(c) ) ) from ORDINAL2:sch_2();
take  S | a ; ::_thesis: ex S2 being T-Sequence st
( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b )
take  S2 ; ::_thesis: ( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b )
set s = (S | a) ^ S2;
A4: dom S = dom ((S | a) ^ S2) by A1, A2, A3, ORDINAL4:def_1;
now__::_thesis:_for_x_being_set_st_x_in_dom_S_holds_
S_._x_=_((S_|_a)_^_S2)_._x
let x be set ; ::_thesis: ( x in dom S implies S . b1 = ((S | a) ^ S2) . b1 )
assume A5: x in dom S ; ::_thesis: S . b1 = ((S | a) ^ S2) . b1
then reconsider z = x as Ordinal ;
percases ( z in a or ex c being ordinal number st
( c in b & z = a +^ c ) ) by A1, A5, ORDINAL3:38;
supposeA6: z in a ; ::_thesis: S . b1 = ((S | a) ^ S2) . b1
hence S . x = (S | a) . z by FUNCT_1:49
.= ((S | a) ^ S2) . x by A6, A2, ORDINAL4:def_1 ;
::_thesis: verum
end;
suppose ex c being ordinal number st
( c in b & z = a +^ c ) ; ::_thesis: S . b1 = ((S | a) ^ S2) . b1
then consider c being ordinal number  such that
A7: ( c in b & z = a +^ c ) ;
thus S . x = S2 . c by A3, A7
.= ((S | a) ^ S2) . x by A7, A2, A3, ORDINAL4:def_1 ; ::_thesis: verum
end;
end;
end;
hence  ( S = (S | a) ^ S2 & dom (S | a) = a & dom S2 = b ) by B2, A3, A4, FUNCT_1:2, A1, RELAT_1:62; ::_thesis: verum
end;

theorem Th3: :: ORDINAL5:3
for S1, S2 being T-Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )
proof
let S1, S2 be T-Sequence; ::_thesis: ( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )
set q = S1 ^ S2;
A1: dom (S1 ^ S2) = (dom S1) +^ (dom S2) by ORDINAL4:def_1;
then A2: dom S1 c= dom (S1 ^ S2) by ORDINAL3:24;
thus  rng S1 c= rng (S1 ^ S2) ::_thesis: rng S2 c= rng (S1 ^ S2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng S1 or x in rng (S1 ^ S2) )
assume  x in rng S1 ; ::_thesis: x in rng (S1 ^ S2)
then consider z being set  such that
A3: ( z in dom S1 & x = S1 . z ) by FUNCT_1:def_3;
reconsider z = z as Ordinal by A3;
 ( (S1 ^ S2) . z = x & z in dom (S1 ^ S2) ) by A3, A2, ORDINAL4:def_1;
hence  x in rng (S1 ^ S2) by FUNCT_1:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng S2 or x in rng (S1 ^ S2) )
assume  x in rng S2 ; ::_thesis: x in rng (S1 ^ S2)
then consider z being set  such that
A4: ( z in dom S2 & x = S2 . z ) by FUNCT_1:def_3;
reconsider z = z as Ordinal by A4;
 ( (S1 ^ S2) . ((dom S1) +^ z) = x & (dom S1) +^ z in dom (S1 ^ S2) ) by A1, A4, ORDINAL3:17, ORDINAL4:def_1;
hence  x in rng (S1 ^ S2) by FUNCT_1:def_3; ::_thesis: verum
end;

theorem Th4: :: ORDINAL5:4
for S1, S2 being T-Sequence st S1 ^ S2 is Ordinal-yielding holds
( S1 is Ordinal-yielding & S2 is Ordinal-yielding )
proof
let S1, S2 be T-Sequence; ::_thesis: ( S1 ^ S2 is Ordinal-yielding implies ( S1 is Ordinal-yielding & S2 is Ordinal-yielding ) )
given a being ordinal number  such that A1: rng (S1 ^ S2) c= a ; :: according to ORDINAL2:def_4 ::_thesis: ( S1 is Ordinal-yielding & S2 is Ordinal-yielding )
thus  S1 is Ordinal-yielding ::_thesis: S2 is Ordinal-yielding
proof
take  a ; :: according to ORDINAL2:def_4 ::_thesis: rng S1 c= a
 rng S1 c= rng (S1 ^ S2) by Th3;
hence  rng S1 c= a by A1, XBOOLE_1:1; ::_thesis: verum
end;
take  a ; :: according to ORDINAL2:def_4 ::_thesis: rng S2 c= a
 rng S2 c= rng (S1 ^ S2) by Th3;
hence  rng S2 c= a by A1, XBOOLE_1:1; ::_thesis: verum
end;

definition
let f be T-Sequence;
attrf is decreasing  means :: ORDINAL5:def 1
 for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a;
attrf is non-decreasing  means :Def2: :: ORDINAL5:def 2
 for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b;
attrf is non-increasing  means :: ORDINAL5:def 3
 for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a;
end;

:: deftheorem  defines decreasing ORDINAL5:def_1_:_
 for f being T-Sequence holds
( f is decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a );

:: deftheorem Def2 defines non-decreasing ORDINAL5:def_2_:_
 for f being T-Sequence holds
( f is non-decreasing iff for a, b being ordinal number st a in b & b in dom f holds
f . a c= f . b );

:: deftheorem  defines non-increasing ORDINAL5:def_3_:_
 for f being T-Sequence holds
( f is non-increasing iff for a, b being ordinal number st a in b & b in dom f holds
f . b c= f . a );

registration
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding increasing  ->  non-decreasing for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is increasing holds
b1 is non-decreasing
proof
let f be Ordinal-Sequence; ::_thesis: ( f is increasing implies f is non-decreasing )
assume A1: for a, b being ordinal number st a in b & b in dom f holds
f . a in f . b ; :: according to ORDINAL2:def_12 ::_thesis: f is non-decreasing
let a be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st a in b & b in dom f holds
f . a c= f . b
let b be ordinal number ; ::_thesis: ( a in b & b in dom f implies f . a c= f . b )
 ( f . a in f . b implies f . a c= f . b ) by ORDINAL1:def_2;
hence  ( a in b & b in dom f implies f . a c= f . b ) by A1; ::_thesis: verum
end;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding decreasing  ->  non-increasing for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is decreasing holds
b1 is non-increasing
proof
let f be Ordinal-Sequence; ::_thesis: ( f is decreasing implies f is non-increasing )
assume A2: for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a ; :: according to ORDINAL5:def_1 ::_thesis: f is non-increasing
let a be ordinal number ; :: according to ORDINAL5:def_3 ::_thesis: for b being ordinal number st a in b & b in dom f holds
f . b c= f . a
let b be ordinal number ; ::_thesis: ( a in b & b in dom f implies f . b c= f . a )
 ( f . b in f . a implies f . b c= f . a ) by ORDINAL1:def_2;
hence  ( a in b & b in dom f implies f . b c= f . a ) by A2; ::_thesis: verum
end;
end;

theorem Th5: :: ORDINAL5:5
for f being T-Sequence holds
( f is infinite iff omega c= dom f )
proof
let f be T-Sequence; ::_thesis: ( f is infinite iff omega c= dom f )
 ( f is infinite iff dom f is infinite ) by FINSET_1:10;
hence  ( f is infinite iff omega c= dom f ) by CARD_3:85; ::_thesis: verum
end;

registration
cluster Relation-like Function-like T-Sequence-like decreasing  ->  finite for set ;
coherence
 for b1 being T-Sequence st b1 is decreasing holds
b1 is finite
proof
let f be T-Sequence; ::_thesis: ( f is decreasing implies f is finite )
assume A1: for a, b being ordinal number st a in b & b in dom f holds
f . b in f . a ; :: according to ORDINAL5:def_1 ::_thesis: f is finite
set X = f .: omega;
assume  f is infinite ; ::_thesis: contradiction
then A2: ( 0 in omega & omega c= dom f ) by Th5;
then  f . 0 in f .: omega by FUNCT_1:def_6;
then consider x being set  such that
A3: ( x in f .: omega & f .: omega misses x ) by XREGULAR:1;
consider a being set  such that
A4: ( a in dom f & a in omega & x = f . a ) by A3, FUNCT_1:def_6;
reconsider a = a as Ordinal by A4;
A5: succ a in omega by A4, ORDINAL1:28;
then  ( a in succ a & succ a in dom f ) by A2, ORDINAL1:6;
then  ( f . (succ a) in x & f . (succ a) in f .: omega ) by A1, A4, A5, FUNCT_1:def_6;
hence  contradiction by A3, XBOOLE_0:3; ::_thesis: verum
end;
cluster empty  ->  empty increasing decreasing for set ;
coherence
 for b1 being empty set holds
( b1 is decreasing & b1 is increasing )
proof
let e be empty set ; ::_thesis: ( e is decreasing & e is increasing )
thus  e is decreasing ::_thesis: e is increasing
proof
let a be ordinal number ; :: according to ORDINAL5:def_1 ::_thesis: for b being ordinal number st a in b & b in dom e holds
e . b in e . a
thus  for b being ordinal number st a in b & b in dom e holds
e . b in e . a ; ::_thesis: verum
end;
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom e or e . a in e . b1 )
thus  for b1 being set holds
( not a in b1 or not b1 in dom e or e . a in e . b1 ) ; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
cluster<%a%> ->  Ordinal-yielding ;
coherence
 <%a%> is Ordinal-yielding
proof
take  succ a ; :: according to ORDINAL2:def_4 ::_thesis: rng <%a%> c= succ a
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng <%a%> or x in succ a )
assume  x in rng <%a%> ; ::_thesis: x in succ a
then  x in {a} by AFINSQ_1:33;
then  x = a by TARSKI:def_1;
hence  x in succ a by ORDINAL1:6; ::_thesis: verum
end;
end;

registration
let a be ordinal number ;
cluster<%a%> ->  increasing decreasing ;
coherence
 ( <%a%> is decreasing & <%a%> is increasing )
proof
set f = <%a%>;
A1: ( dom <%a%> = 1 & <%a%> . 0 = a ) by AFINSQ_1:def_4;
hence  for c, b being ordinal number st c in b & b in dom <%a%> holds
<%a%> . b in <%a%> . c by ORDINAL3:15, TARSKI:def_1; :: according to ORDINAL5:def_1 ::_thesis: <%a%> is increasing
let c be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not c in b1 or not b1 in dom <%a%> or <%a%> . c in <%a%> . b1 )
let b be ordinal number ; ::_thesis: ( not c in b or not b in dom <%a%> or <%a%> . c in <%a%> . b )
thus  ( not c in b or not b in dom <%a%> or <%a%> . c in <%a%> . b ) by A1, ORDINAL3:15, TARSKI:def_1; ::_thesis: verum
end;
end;

registration
cluster Relation-like Function-like non empty T-Sequence-like finite Ordinal-yielding increasing decreasing non-decreasing non-increasing for set ;
existence
 ex b1 being Ordinal-Sequence st
( b1 is decreasing & b1 is increasing & b1 is non-decreasing & b1 is non-increasing & b1 is finite & not b1 is empty )
proof
set a = the ordinal number ;
take  <% the ordinal number %> ; ::_thesis: ( <% the ordinal number %> is decreasing & <% the ordinal number %> is increasing & <% the ordinal number %> is non-decreasing & <% the ordinal number %> is non-increasing & <% the ordinal number %> is finite & not <% the ordinal number %> is empty )
thus  ( <% the ordinal number %> is decreasing & <% the ordinal number %> is increasing & <% the ordinal number %> is non-decreasing & <% the ordinal number %> is non-increasing & <% the ordinal number %> is finite & not <% the ordinal number %> is empty ) ; ::_thesis: verum
end;
end;

theorem Th6: :: ORDINAL5:6
for f being non-decreasing Ordinal-Sequence st not dom f is empty holds
Union f is_limes_of f
proof
let f be non-decreasing Ordinal-Sequence; ::_thesis: ( not dom f is empty implies Union f is_limes_of f )
assume A1: not dom f is empty ; ::_thesis: Union f is_limes_of f
set a0 = the Element of dom f;
percases ( Union f = {} or Union f <> {} ) ;
:: according to ORDINAL2:def_9
caseA2: Union f = {} ; ::_thesis: ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or f . b2 = {} ) ) )
take  the Element of dom f ; ::_thesis: ( the Element of dom f in dom f & ( for b1 being set holds
( not the Element of dom f c= b1 or not b1 in dom f or f . b1 = {} ) ) )
thus  the Element of dom f in dom f by A1; ::_thesis: for b1 being set holds
( not the Element of dom f c= b1 or not b1 in dom f or f . b1 = {} )
let c be ordinal number ; ::_thesis: ( not the Element of dom f c= c or not c in dom f or f . c = {} )
assume  ( the Element of dom f c= c & c in dom f ) ; ::_thesis: f . c = {}
then  f . c in rng f by FUNCT_1:def_3;
hence  f . c = {} by A2, ORDERS_1:6; ::_thesis: verum
end;
case Union f <> {} ; ::_thesis: for b1, b2 being set holds
( not b1 in Union f or not Union f in b2 or ex b3 being set st
( b3 in dom f & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom f or ( b1 in f . b4 & f . b4 in b2 ) ) ) ) )
let b, c be ordinal number ; ::_thesis: ( not b in Union f or not Union f in c or ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or ( b in f . b2 & f . b2 in c ) ) ) ) )
assume A3: ( b in Union f & Union f in c ) ; ::_thesis: ex b1 being set st
( b1 in dom f & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom f or ( b in f . b2 & f . b2 in c ) ) ) )
then consider x being set  such that
A4: ( x in dom f & b in f . x ) by CARD_5:2;
reconsider x = x as Ordinal by A4;
take  x ; ::_thesis: ( x in dom f & ( for b1 being set holds
( not x c= b1 or not b1 in dom f or ( b in f . b1 & f . b1 in c ) ) ) )
thus  x in dom f by A4; ::_thesis: for b1 being set holds
( not x c= b1 or not b1 in dom f or ( b in f . b1 & f . b1 in c ) )
let E be Ordinal; ::_thesis: ( not x c= E or not E in dom f or ( b in f . E & f . E in c ) )
assume A5: ( x c= E & E in dom f ) ; ::_thesis: ( b in f . E & f . E in c )
then  ( x = E or x c< E ) by XBOOLE_0:def_8;
then  ( x = E or x in E ) by ORDINAL1:11;
then  f . x c= f . E by A5, Def2;
hence  b in f . E by A4; ::_thesis: f . E in c
 f . E in rng f by A5, FUNCT_1:def_3;
then  f . E c= Union f by ZFMISC_1:74;
hence  f . E in c by A3, ORDINAL1:12; ::_thesis: verum
end;
end;
end;

theorem :: ORDINAL5:7
for a, b being ordinal number
for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)
proof
let a, b be ordinal number ; ::_thesis: for n being Nat st a in b holds
n *^ (exp (omega,a)) in exp (omega,b)
let n be Nat; ::_thesis: ( a in b implies n *^ (exp (omega,a)) in exp (omega,b) )
assume  a in b ; ::_thesis: n *^ (exp (omega,a)) in exp (omega,b)
then  succ a c= b by ORDINAL1:21;
then A1: exp (omega,(succ a)) c= exp (omega,b) by ORDINAL4:27;
A2: exp (omega,(succ a)) = omega *^ (exp (omega,a)) by ORDINAL2:44;
 n in omega by ORDINAL1:def_12;
then  n *^ (exp (omega,a)) in omega *^ (exp (omega,a)) by ORDINAL3:19, ORDINAL4:22;
hence  n *^ (exp (omega,a)) in exp (omega,b) by A1, A2; ::_thesis: verum
end;

theorem Th8: :: ORDINAL5:8
for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing
proof
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing
let f be Ordinal-Sequence; ::_thesis: ( 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) implies f is non-decreasing )
assume A1: ( 0 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) ) ; ::_thesis: f is non-decreasing
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st b in b & b in dom f holds
f . b c= f . b
let d be ordinal number ; ::_thesis: ( b in d & d in dom f implies f . b c= f . d )
assume A2: ( b in d & d in dom f ) ; ::_thesis: f . b c= f . d
then  b in dom f by ORDINAL1:10;
then  ( b c= d & f . b = exp (a,b) & f . d = exp (a,d) ) by A1, A2, ORDINAL1:def_2;
hence  f . b c= f . d by A1, ORDINAL4:27; ::_thesis: verum
end;

theorem Th9: :: ORDINAL5:9
for a, b being ordinal number st a is limit_ordinal & 0 in b holds
exp (a,b) is limit_ordinal
proof
let a, b be ordinal number ; ::_thesis: ( a is limit_ordinal & 0 in b implies exp (a,b) is limit_ordinal )
assume A1: ( a is limit_ordinal & 0 in b ) ; ::_thesis: exp (a,b) is limit_ordinal
percases ( a = 0 or 0 in a ) by ORDINAL3:8;
suppose a = 0 ; ::_thesis: exp (a,b) is limit_ordinal
hence  exp (a,b) is limit_ordinal by A1, ORDINAL4:20; ::_thesis: verum
end;
supposeA2: 0 in a ; ::_thesis: exp (a,b) is limit_ordinal
defpred S1[ Ordinal] means ( 0 in $1 implies exp (a,$1) is limit_ordinal );
A3: S1[ {} ] ;
A4: for c being ordinal number st S1[c] holds
S1[ succ c]
proof
let c be ordinal number ; ::_thesis: ( S1[c] implies S1[ succ c] )
 exp (a,(succ c)) = a *^ (exp (a,c)) by ORDINAL2:44;
hence  ( S1[c] implies S1[ succ c] ) by A1, ORDINAL3:40; ::_thesis: verum
end;
A5: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) holds
S1[c]
proof
let c be ordinal number ; ::_thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) implies S1[c] )
assume that
A6: ( c <> {} & c is limit_ordinal ) and
A7: for b being ordinal number st b in c holds
S1[b] ; ::_thesis: S1[c]
deffunc H1( Ordinal) ->  set = exp (a,$1);
consider f being Ordinal-Sequence such that
A8: ( dom f = c & ( for b being ordinal number st b in c holds
f . b = H1(b) ) ) from ORDINAL2:sch_3();
A9: exp (a,c) = lim f by A6, A8, ORDINAL2:45;
 f is non-decreasing by A2, A8, Th8;
then  Union f is_limes_of f by A6, A8, Th6;
then A10: exp (a,c) = Union f by A9, ORDINAL2:def_10;
 for d being ordinal number st d in exp (a,c) holds
succ d in exp (a,c)
proof
let d be ordinal number ; ::_thesis: ( d in exp (a,c) implies succ d in exp (a,c) )
assume  d in exp (a,c) ; ::_thesis: succ d in exp (a,c)
then consider b being set  such that
A11: ( b in dom f & d in f . b ) by A10, CARD_5:2;
reconsider b = b as Ordinal by A11;
A12: succ b in dom f by A6, A8, A11, ORDINAL1:28;
then A13: ( f . b = H1(b) & f . (succ b) = H1( succ b) & S1[ succ b] ) by A7, A8, A11;
 H1(b) c= H1( succ b) by A2, ORDINAL3:1, ORDINAL4:27;
then  succ d in f . (succ b) by A13, A11, ORDINAL1:28, ORDINAL3:8;
hence  succ d in exp (a,c) by A10, A12, CARD_5:2; ::_thesis: verum
end;
hence  S1[c] by ORDINAL1:28; ::_thesis: verum
end;
 for c being ordinal number holds S1[c] from ORDINAL2:sch_1(A3, A4, A5);
hence  exp (a,b) is limit_ordinal by A1; ::_thesis: verum
end;
end;
end;

theorem :: ORDINAL5:10
for a being ordinal number
for f being Ordinal-Sequence st 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing
proof
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing
let f be Ordinal-Sequence; ::_thesis: ( 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) implies f is increasing )
assume A1: ( 1 in a & ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) ) ; ::_thesis: f is increasing
let b be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not b in b1 or not b1 in dom f or f . b in f . b1 )
let d be ordinal number ; ::_thesis: ( not b in d or not d in dom f or f . b in f . d )
assume A2: ( b in d & d in dom f ) ; ::_thesis: f . b in f . d
then  ( f . b = exp (a,b) & f . d = exp (a,d) ) by A1, ORDINAL1:10;
hence  f . b in f . d by A1, A2, ORDINAL4:24; ::_thesis: verum
end;

theorem Th11: :: ORDINAL5:11
for a, b being ordinal number
for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
proof
let a, b be ordinal number ; ::_thesis: for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
let x be set ; ::_thesis: ( 0 in a & not b is empty & b is limit_ordinal implies ( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) ) )
assume A1: ( 0 in a & not b is empty & b is limit_ordinal ) ; ::_thesis: ( x in exp (a,b) iff ex c being ordinal number st
( c in b & x in exp (a,c) ) )
deffunc H1( Ordinal) ->  set = exp (a,$1);
consider f being Ordinal-Sequence such that
A2: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch_3();
 f is non-decreasing by A1, A2, Th8;
then  Union f is_limes_of f by A1, A2, Th6;
then A3: Union f = lim f by ORDINAL2:def_10
.= exp (a,b) by A1, A2, ORDINAL2:45 ;
hereby  ::_thesis: ( ex c being ordinal number st
( c in b & x in exp (a,c) ) implies x in exp (a,b) )
assume  x in exp (a,b) ; ::_thesis: ex c being Ordinal st
( c in b & x in exp (a,c) )
then consider c being set  such that
A4: ( c in dom f & x in f . c ) by A3, CARD_5:2;
reconsider c = c as Ordinal by A4;
take c = c; ::_thesis: ( c in b & x in exp (a,c) )
thus  c in b by A2, A4; ::_thesis: x in exp (a,c)
thus  x in exp (a,c) by A2, A4; ::_thesis: verum
end;
given c being ordinal number  such that A5: ( c in b & x in exp (a,c) ) ; ::_thesis: x in exp (a,b)
 f . c = H1(c) by A2, A5;
hence  x in exp (a,b) by A2, A3, A5, CARD_5:2; ::_thesis: verum
end;

theorem Th12: :: ORDINAL5:12
for a, b, c being ordinal number st 0 in a & exp (a,b) in exp (a,c) holds
b in c
proof
let a, b, c be ordinal number ; ::_thesis: ( 0 in a & exp (a,b) in exp (a,c) implies b in c )
assume A1: ( 0 in a & exp (a,b) in exp (a,c) ) ; ::_thesis: b in c
assume  not b in c ; ::_thesis: contradiction
then  exp (a,c) c= exp (a,b) by A1, ORDINAL1:16, ORDINAL4:27;
then  exp (a,b) in exp (a,b) by A1;
hence  contradiction ; ::_thesis: verum
end;

begin

definition
let a, b be Ordinal;
funca |^|^ b ->  Ordinal means :Def4: :: ORDINAL5:def 4
 ex phi being Ordinal-Sequence st
( it = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
correctness
existence
ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
uniqueness
for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal) ->  set = exp (a,$2);
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
 ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ b & fi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
fi . (succ c) = H1(c,fi . c) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ b & fi . {} = 1 & ( for C being Ordinal st succ C in succ b holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ b & fi . {} = 1 & ( for C being Ordinal st succ C in succ b holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ b & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence  ( ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ( for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines |^|^ ORDINAL5:def_4_:_
 for a, b, b3 being Ordinal holds
( b3 = a |^|^ b iff ex phi being Ordinal-Sequence st
( b3 = last phi & dom phi = succ b & phi . {} = 1 & ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) & ( for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th13: :: ORDINAL5:13
for a being ordinal number holds a |^|^ 0 = 1
proof
let a be ordinal number ; ::_thesis: a |^|^ 0 = 1
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  set = exp (a,$2);
A1: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = 1 & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def4;
thus  H1( {} ) = 1 from ORDINAL2:sch_14(A1); ::_thesis: verum
end;

theorem Th14: :: ORDINAL5:14
for a, b being ordinal number holds a |^|^ (succ b) = exp (a,(a |^|^ b))
proof
let a, b be ordinal number ; ::_thesis: a |^|^ (succ b) = exp (a,(a |^|^ b))
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  set = exp (a,$2);
A1: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = 1 & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def4;
 for b being ordinal number holds H1( succ b) = H3(b,H1(b)) from ORDINAL2:sch_15(A1);
hence  a |^|^ (succ b) = exp (a,(a |^|^ b)) ; ::_thesis: verum
end;

theorem Th15: :: ORDINAL5:15
for b, a being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi
proof
let b, a be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi )
assume A1: ( b <> {} & b is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  set = exp (a,$2);
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = b & ( for c being ordinal number st c in b holds
fi . c = a |^|^ c ) implies a |^|^ b = lim fi )
assume that
A2: dom fi = b and
A3: for c being ordinal number st c in b holds
fi . c = H1(c) ; ::_thesis: a |^|^ b = lim fi
A4: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = 1 & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def4;
thus  H1(b) = H2(b,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;

theorem Th16: :: ORDINAL5:16
for a being ordinal number holds a |^|^ 1 = a
proof
let a be ordinal number ; ::_thesis: a |^|^ 1 = a
 0 + 1 = succ 0 ;
hence a |^|^ 1 = exp (a,(a |^|^ 0)) by Th14
.= exp (a,1) by Th13
.= a by ORDINAL2:46 ;
::_thesis: verum
end;

theorem Th17: :: ORDINAL5:17
for a being ordinal number holds 1 |^|^ a = 1
proof
let a be ordinal number ; ::_thesis: 1 |^|^ a = 1
defpred S1[ Ordinal] means 1 |^|^ $1 = 1;
A1: S1[ {} ] by Th13;
A2: for a being ordinal number st S1[a] holds
S1[ succ a]
proof
let A be Ordinal; ::_thesis: ( S1[A] implies S1[ succ A] )
assume  S1[A] ; ::_thesis: S1[ succ A]
hence 1 |^|^ (succ A) = exp (1,1) by Th14
.= 1 by ORDINAL2:46 ;
::_thesis: verum
end;
A3: for A being Ordinal st A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) holds
S1[A]
proof
let A be Ordinal; ::_thesis: ( A <> {} & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
assume that
A4: ( A <> {} & A is limit_ordinal ) and
A5: for B being Ordinal st B in A holds
1 |^|^ B = 1 ; ::_thesis: S1[A]
deffunc H1( Ordinal) ->  Ordinal = 1 |^|^ $1;
consider fi being Ordinal-Sequence such that
A6: ( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) ) from ORDINAL2:sch_3();
A7: 1 |^|^ A = lim fi by A4, A6, Th15;
A8: rng fi c= {1}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng fi or x in {1} )
assume  x in rng fi ; ::_thesis: x in {1}
then consider y being set  such that
A9: ( y in dom fi & x = fi . y ) by FUNCT_1:def_3;
reconsider y = y as Ordinal by A9;
x = 1 |^|^ y by A6, A9
.= 1 by A5, A6, A9 ;
hence  x in {1} by TARSKI:def_1; ::_thesis: verum
end;
now__::_thesis:_(_{}_<>_1_&_(_for_b,_c_being_ordinal_number_st_b_in_1_&_1_in_c_holds_
ex_D_being_Ordinal_st_
(_D_in_dom_fi_&_(_for_E_being_Ordinal_st_D_c=_E_&_E_in_dom_fi_holds_
(_b_in_fi_._E_&_fi_._E_in_c_)_)_)_)_)
thus  {} <> 1 ; ::_thesis: for b, c being ordinal number st b in 1 & 1 in c holds
ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
let b, c be ordinal number ; ::_thesis: ( b in 1 & 1 in c implies ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) ) )
assume A10: ( b in 1 & 1 in c ) ; ::_thesis: ex D being Ordinal st
( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
set x = the Element of A;
reconsider x = the Element of A as Ordinal ;
take D = x; ::_thesis: ( D in dom fi & ( for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c ) ) )
thus  D in dom fi by A4, A6; ::_thesis: for E being Ordinal st D c= E & E in dom fi holds
( b in fi . E & fi . E in c )
let E be Ordinal; ::_thesis: ( D c= E & E in dom fi implies ( b in fi . E & fi . E in c ) )
assume  ( D c= E & E in dom fi ) ; ::_thesis: ( b in fi . E & fi . E in c )
then  fi . E in rng fi by FUNCT_1:def_3;
hence  ( b in fi . E & fi . E in c ) by A8, A10, TARSKI:def_1; ::_thesis: verum
end;
then  1 is_limes_of fi by ORDINAL2:def_9;
hence  1 |^|^ A = 1 by A7, ORDINAL2:def_10; ::_thesis: verum
end;
 for a being ordinal number holds S1[a] from ORDINAL2:sch_1(A1, A2, A3);
hence  1 |^|^ a = 1 ; ::_thesis: verum
end;

theorem Th18: :: ORDINAL5:18
for a being ordinal number holds a |^|^ 2 = exp (a,a)
proof
let a be ordinal number ; ::_thesis: a |^|^ 2 = exp (a,a)
 2 = succ 1 ;
hence a |^|^ 2 = exp (a,(a |^|^ 1)) by Th14
.= exp (a,a) by Th16 ;
::_thesis: verum
end;

theorem :: ORDINAL5:19
for a being ordinal number holds a |^|^ 3 = exp (a,(exp (a,a)))
proof
let a be ordinal number ; ::_thesis: a |^|^ 3 = exp (a,(exp (a,a)))
 3 = succ 2 ;
hence a |^|^ 3 = exp (a,(a |^|^ 2)) by Th14
.= exp (a,(exp (a,a))) by Th18 ;
::_thesis: verum
end;

theorem :: ORDINAL5:20
for n being Nat holds
( 0 |^|^ (2 * n) = 1 & 0 |^|^ ((2 * n) + 1) = 0 )
proof
defpred S1[ Nat] means ( 0 |^|^ (2 * $1) = 1 & 0 |^|^ ((2 * $1) + 1) = 0 );
A1: S1[ 0 ] by Th13, Th16;
A2: 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 A3: S1[n] ; ::_thesis: S1[n + 1]
thus  S1[n + 1] ::_thesis: verum
proof
thus A4: 0 |^|^ (2 * (n + 1)) = 0 |^|^ (((2 * n) + 1) + 1)
.= 0 |^|^ (succ ((2 * n) + 1)) by NAT_1:def_2
.= exp (0,0) by A3, Th14
.= 1 by ORDINAL2:43 ; ::_thesis: 0 |^|^ ((2 * (n + 1)) + 1) = 0
thus 0 |^|^ ((2 * (n + 1)) + 1) = 0 |^|^ (succ (2 * (n + 1))) by NAT_1:def_2
.= exp (0,1) by A4, Th14
.= 0 by ORDINAL2:46 ; ::_thesis: verum
end;
end;
thus  for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2); ::_thesis: verum
end;

theorem Th21: :: ORDINAL5:21
for a, b, c being ordinal number st a c= b & 0 in c holds
c |^|^ a c= c |^|^ b
proof
let a, b, c be ordinal number ; ::_thesis: ( a c= b & 0 in c implies c |^|^ a c= c |^|^ b )
assume that
A1: a c= b and
A2: 0 in c ; ::_thesis: c |^|^ a c= c |^|^ b
 ( succ 0 c= c & succ 0 = 0 + 1 ) by A2, ORDINAL1:21;
then A3: ( 1 c< c or 1 = c ) by XBOOLE_0:def_8;
percases ( c = 1 or 1 in c ) by A3, ORDINAL1:11;
suppose c = 1 ; ::_thesis: c |^|^ a c= c |^|^ b
then  ( c |^|^ a = 1 & c |^|^ b = 1 ) by Th17;
hence  c |^|^ a c= c |^|^ b ; ::_thesis: verum
end;
supposeA4: 1 in c ; ::_thesis: c |^|^ a c= c |^|^ b
defpred S1[ Ordinal] means  for a, b being ordinal number st a c= b & b c= $1 holds
c |^|^ a c= c |^|^ b;
A5: S1[ {} ]
proof
let a, b be ordinal number ; ::_thesis: ( a c= b & b c= {} implies c |^|^ a c= c |^|^ b )
assume A6: ( a c= b & b c= {} ) ; ::_thesis: c |^|^ a c= c |^|^ b
then  b = {} ;
hence  c |^|^ a c= c |^|^ b by A6; ::_thesis: verum
end;
A7: now__::_thesis:_for_d_being_ordinal_number_st_S1[d]_holds_
S1[_succ_d]
let d be ordinal number ; ::_thesis: ( S1[d] implies S1[ succ d] )
assume A8: S1[d] ; ::_thesis: S1[ succ d]
 c |^|^ (succ d) = exp (c,(c |^|^ d)) by Th14;
then A9: c |^|^ d c= c |^|^ (succ d) by A4, ORDINAL4:32;
thus  S1[ succ d] ::_thesis: verum
proof
let a, b be ordinal number ; ::_thesis: ( a c= b & b c= succ d implies c |^|^ a c= c |^|^ b )
assume A10: ( a c= b & b c= succ d ) ; ::_thesis: c |^|^ a c= c |^|^ b
A11: a c= succ d by A10, XBOOLE_1:1;
percases ( b c= d or ( b = succ d & a = succ d ) or ( b = succ d & a c= d ) ) by A10, A11, Th1;
suppose b c= d ; ::_thesis: c |^|^ a c= c |^|^ b
hence  c |^|^ a c= c |^|^ b by A8, A10; ::_thesis: verum
end;
suppose ( b = succ d & a = succ d ) ; ::_thesis: c |^|^ a c= c |^|^ b
hence  c |^|^ a c= c |^|^ b ; ::_thesis: verum
end;
supposeA12: ( b = succ d & a c= d ) ; ::_thesis: c |^|^ a c= c |^|^ b
then  c |^|^ a c= c |^|^ d by A8;
hence  c |^|^ a c= c |^|^ b by A9, A12, XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
end;
A13: now__::_thesis:_for_d_being_ordinal_number_st_d_<>_{}_&_d_is_limit_ordinal_&_(_for_e_being_ordinal_number_st_e_in_d_holds_
S1[e]_)_holds_
S1[d]
let d be ordinal number ; ::_thesis: ( d <> {} & d is limit_ordinal & ( for e being ordinal number st e in d holds
S1[e] ) implies S1[d] )
assume that
A14: ( d <> {} & d is limit_ordinal ) and
A15: for e being ordinal number st e in d holds
S1[e] ; ::_thesis: S1[d]
deffunc H1( Ordinal) ->  Ordinal = c |^|^ $1;
consider f being Ordinal-Sequence such that
A16: ( dom f = d & ( for e being ordinal number st e in d holds
f . e = H1(e) ) ) from ORDINAL2:sch_3();
 f is non-decreasing
proof
let a be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st a in b & b in dom f holds
f . a c= f . b
let b be ordinal number ; ::_thesis: ( a in b & b in dom f implies f . a c= f . b )
assume A17: ( a in b & b in dom f ) ; ::_thesis: f . a c= f . b
then  ( a c= b & S1[b] ) by A15, A16, ORDINAL1:def_2;
then  ( c |^|^ a c= c |^|^ b & a in d & f . b = H1(b) ) by A16, A17, ORDINAL1:12;
hence  f . a c= f . b by A16; ::_thesis: verum
end;
then A18: Union f is_limes_of f by A14, A16, Th6;
 c |^|^ d = lim f by A14, A16, Th15;
then A19: c |^|^ d = Union f by A18, ORDINAL2:def_10;
thus  S1[d] ::_thesis: verum
proof
let a, b be ordinal number ; ::_thesis: ( a c= b & b c= d implies c |^|^ a c= c |^|^ b )
assume A20: ( a c= b & b c= d ) ; ::_thesis: c |^|^ a c= c |^|^ b
then A21: ( ( b c< d or b = d ) & ( a c< b or a = b ) ) by XBOOLE_0:def_8;
percases ( b in d or ( b = d & a in d ) or ( b = d & a = d ) ) by A21, ORDINAL1:11;
suppose b in d ; ::_thesis: c |^|^ a c= c |^|^ b
hence  H1(a) c= H1(b) by A20, A15; ::_thesis: verum
end;
supposeA22: ( b = d & a in d ) ; ::_thesis: c |^|^ a c= c |^|^ b
then  ( f . a in rng f & f . a = H1(a) ) by A16, FUNCT_1:def_3;
hence  H1(a) c= H1(b) by A19, A22, ZFMISC_1:74; ::_thesis: verum
end;
suppose ( b = d & a = d ) ; ::_thesis: c |^|^ a c= c |^|^ b
hence  H1(a) c= H1(b) ; ::_thesis: verum
end;
end;
end;
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A5, A7, A13);
hence  c |^|^ a c= c |^|^ b by A1; ::_thesis: verum
end;
end;
end;

theorem :: ORDINAL5:22
for a being ordinal number
for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing
proof
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st 0 in a & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing
let f be Ordinal-Sequence; ::_thesis: ( 0 in a & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) implies f is non-decreasing )
assume that
A1: 0 in a and
A2: for b being ordinal number st b in dom f holds
f . b = a |^|^ b ; ::_thesis: f is non-decreasing
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st b in b & b in dom f holds
f . b c= f . b
let c be ordinal number ; ::_thesis: ( b in c & c in dom f implies f . b c= f . c )
assume A3: ( b in c & c in dom f ) ; ::_thesis: f . b c= f . c
then  b c= c by ORDINAL1:def_2;
then  ( a |^|^ b c= a |^|^ c & a |^|^ c = f . c ) by A1, A2, A3, Th21;
hence  f . b c= f . c by A2, A3, ORDINAL1:10; ::_thesis: verum
end;

theorem Th23: :: ORDINAL5:23
for a, b being ordinal number st 0 in a & 0 in b holds
a c= a |^|^ b
proof
let a, b be ordinal number ; ::_thesis: ( 0 in a & 0 in b implies a c= a |^|^ b )
assume A1: ( 0 in a & 0 in b ) ; ::_thesis: a c= a |^|^ b
defpred S1[ Ordinal] means ( 0 in $1 implies a c= a |^|^ $1 );
A2: S1[ 0 ] ;
A3: now__::_thesis:_for_b_being_ordinal_number_st_S1[b]_holds_
S1[_succ_b]
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume A4: S1[b] ; ::_thesis: S1[ succ b]
A5: a |^|^ (succ b) = exp (a,(a |^|^ b)) by Th14;
A6: succ 0 = 0 + 1 ;
thus  S1[ succ b] ::_thesis: verum
proof
percases ( 0 in b or b = 0 ) by ORDINAL3:8;
suppose 0 in b ; ::_thesis: S1[ succ b]
then  1 c= a |^|^ b by A6, A1, A4, ORDINAL1:21;
then  exp (a,1) c= exp (a,(a |^|^ b)) by A1, ORDINAL4:27;
hence  S1[ succ b] by A5, ORDINAL2:46; ::_thesis: verum
end;
suppose b = 0 ; ::_thesis: S1[ succ b]
then  a |^|^ b = 1 by Th13;
hence  S1[ succ b] by A5, ORDINAL2:46; ::_thesis: verum
end;
end;
end;
end;
A7: now__::_thesis:_for_c_being_ordinal_number_st_c_<>_{}_&_c_is_limit_ordinal_&_(_for_b_being_ordinal_number_st_b_in_c_holds_
S1[b]_)_holds_
S1[c]
let c be ordinal number ; ::_thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) implies S1[c] )
assume A8: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) ) ; ::_thesis: S1[c]
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A9: ( dom phi = c & ( for b being ordinal number st b in c holds
phi . b = H1(b) ) ) from ORDINAL2:sch_3();
 phi is non-decreasing
proof
let e be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st e in b & b in dom phi holds
phi . e c= phi . b
let b be ordinal number ; ::_thesis: ( e in b & b in dom phi implies phi . e c= phi . b )
assume A10: ( e in b & b in dom phi ) ; ::_thesis: phi . e c= phi . b
then A11: ( phi . b = H1(b) & e in c ) by A9, ORDINAL1:10;
then  ( phi . e = H1(e) & e c= b ) by A9, A10, ORDINAL1:def_2;
hence  phi . e c= phi . b by A1, A11, Th21; ::_thesis: verum
end;
then A12: Union phi is_limes_of phi by A8, A9, Th6;
 lim phi = H1(c) by A8, A9, Th15;
then A13: H1(c) = Union phi by A12, ORDINAL2:def_10;
thus  S1[c] ::_thesis: verum
proof
assume  0 in c ; ::_thesis: a c= a |^|^ c
then  succ 0 in c by A8, ORDINAL1:28;
then  ( phi . 1 in rng phi & phi . 1 = H1(1) & H1(1) = a ) by A9, Th16, FUNCT_1:def_3;
hence  a c= a |^|^ c by A13, ZFMISC_1:74; ::_thesis: verum
end;
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A2, A3, A7);
hence  a c= a |^|^ b by A1; ::_thesis: verum
end;

theorem Th24: :: ORDINAL5:24
for a being ordinal number
for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n
proof
let a be ordinal number ; ::_thesis: for m, n being Nat st 1 in a & m < n holds
a |^|^ m in a |^|^ n
let m, n be Nat; ::_thesis: ( 1 in a & m < n implies a |^|^ m in a |^|^ n )
assume A1: ( 1 in a & m < n ) ; ::_thesis: a |^|^ m in a |^|^ n
then  m + 1 <= n by NAT_1:13;
then consider k being Nat such that
A2: n = (m + 1) + k by NAT_1:10;
defpred S1[ Nat] means a |^|^ $1 in a |^|^ ($1 + 1);
defpred S2[ Nat] means a |^|^ m in a |^|^ ((m + 1) + $1);
 a |^|^ 0 = 1 by Th13;
then A3: S1[ 0 ] by A1, Th16;
A4: 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 B4: S1[n] ; ::_thesis: S1[n + 1]
 ( succ n = n + 1 & succ (n + 1) = (n + 1) + 1 ) by NAT_1:38;
then  ( a |^|^ (n + 1) = exp (a,(a |^|^ n)) & a |^|^ ((n + 1) + 1) = exp (a,(a |^|^ (n + 1))) ) by Th14;
hence  S1[n + 1] by B4, A1, ORDINAL4:24; ::_thesis: verum
end;
A6: for n being Nat holds S1[n] from NAT_1:sch_2(A3, A4);
then A7: S2[ 0 ] ;
A8: now__::_thesis:_for_k_being_Nat_st_S2[k]_holds_
S2[k_+_1]
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
assume A9: S2[k] ; ::_thesis: S2[k + 1]
 a |^|^ ((m + 1) + k) in a |^|^ (((m + 1) + k) + 1) by A6;
hence  S2[k + 1] by A9, ORDINAL1:10; ::_thesis: verum
end;
 for k being Nat holds S2[k] from NAT_1:sch_2(A7, A8);
hence  a |^|^ m in a |^|^ n by A2; ::_thesis: verum
end;

theorem Th25: :: ORDINAL5:25
for a being ordinal number
for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing
proof
let a be ordinal number ; ::_thesis: for f being Ordinal-Sequence st 1 in a & dom f c= omega & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing
let f be Ordinal-Sequence; ::_thesis: ( 1 in a & dom f c= omega & ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) implies f is increasing )
assume that
A1: 1 in a and
A2: dom f c= omega and
A3: for n being Ordinal st n in dom f holds
f . n = a |^|^ n ; ::_thesis: f is increasing
let b be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not b in b1 or not b1 in dom f or f . b in f . b1 )
let c be ordinal number ; ::_thesis: ( not b in c or not c in dom f or f . b in f . c )
assume A4: ( b in c & c in dom f ) ; ::_thesis: f . b in f . c
then A5: b in dom f by ORDINAL1:10;
reconsider b = b, c = c as Element of omega by A2, A4, ORDINAL1:10;
 ( f . b = a |^|^ b & f . c = a |^|^ c & b < c ) by A3, A4, A5, NAT_1:44;
hence  f . b in f . c by A1, Th24; ::_thesis: verum
end;

theorem Th26: :: ORDINAL5:26
for a, b being ordinal number st 1 in a & 1 in b holds
a in a |^|^ b
proof
let a, b be ordinal number ; ::_thesis: ( 1 in a & 1 in b implies a in a |^|^ b )
assume A1: 1 in a ; ::_thesis: ( not 1 in b or a in a |^|^ b )
assume  1 in b ; ::_thesis: a in a |^|^ b
then B2: succ 1 c= b by ORDINAL1:21;
 0 in 1 by NAT_1:44;
then  0 in a by A1, ORDINAL1:10;
then  ( a |^|^ 1 in a |^|^ 2 & a |^|^ 2 c= a |^|^ b ) by A1, B2, Th21, Th24;
then  a |^|^ 1 in a |^|^ b ;
hence  a in a |^|^ b by Th16; ::_thesis: verum
end;

theorem Th27: :: ORDINAL5:27
for n, k being Nat holds exp (n,k) = n |^ k
proof
let n be Nat; ::_thesis: for k being Nat holds exp (n,k) = n |^ k
defpred S1[ Nat] means  exp (n,$1) = n |^ $1;
 exp (n,0) = 1 by ORDINAL2:43;
then A1: S1[ 0 ] by NEWTON:4;
A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
reconsider n9 = n, nk = n |^ k as Element of NAT by ORDINAL1:def_12;
 k + 1 = succ k by NAT_1:38;
then  exp (n,(k + 1)) = n *^ (exp (n,k)) by ORDINAL2:44
.= n9 * nk by A3, CARD_2:37 ;
hence  S1[k + 1] by NEWTON:6; ::_thesis: verum
end;
thus  for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2); ::_thesis: verum
end;

registration
let n, k be Nat;
cluster exp (n,k) ->  natural ;
coherence
 exp (n,k) is natural
proof
 exp (n,k) = n |^ k by Th27;
hence  exp (n,k) is natural ; ::_thesis: verum
end;
end;

registration
let n, k be Nat;
clustern |^|^ k ->  natural ;
coherence
 n |^|^ k is natural
proof
defpred S1[ Nat] means n |^|^ n is natural ;
A1: S1[ 0 ] by Th13;
A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume  S1[k] ; ::_thesis: S1[k + 1]
then reconsider nk = n |^|^ k as Nat ;
 k + 1 = succ k by NAT_1:38;
then  n |^|^ (k + 1) = exp (n,nk) by Th14;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A1, A2);
hence  n |^|^ k is natural ; ::_thesis: verum
end;
end;

theorem Th28: :: ORDINAL5:28
for n, k being Nat st n > 1 holds
n |^|^ k > k
proof
let n, k be Nat; ::_thesis: ( n > 1 implies n |^|^ k > k )
assume A1: n > 1 ; ::_thesis: n |^|^ k > k
defpred S1[ Nat] means n |^|^ $1 > $1;
A2: S1[ 0 ] by Th13;
A3: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_
S1[k_+_1]
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; ::_thesis: S1[k + 1]
 succ k = k + 1 by NAT_1:38;
then n |^|^ (k + 1) = exp (n,(n |^|^ k)) by Th14
.= n |^ (n |^|^ k) by Th27 ;
then A5: n |^|^ (k + 1) > n |^ k by A1, A4, PEPIN:66;
 n |^ k > k by A1, NAT_4:3;
then  n |^ k >= k + 1 by NAT_1:13;
hence  S1[k + 1] by A5, XXREAL_0:2; ::_thesis: verum
end;
 for k being Nat holds S1[k] from NAT_1:sch_2(A2, A3);
hence  n |^|^ k > k ; ::_thesis: verum
end;

theorem :: ORDINAL5:29
for n being Nat st n > 1 holds
n |^|^ omega = omega
proof
let n be Nat; ::_thesis: ( n > 1 implies n |^|^ omega = omega )
assume A1: n > 1 ; ::_thesis: n |^|^ omega = omega
deffunc H1( Ordinal) ->  Ordinal = n |^|^ $1;
consider phi being Ordinal-Sequence such that
A2: ( dom phi = omega & ( for b being ordinal number st b in omega holds
phi . b = H1(b) ) ) from ORDINAL2:sch_3();
A3: rng phi c= omega
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng phi or x in omega )
assume  x in rng phi ; ::_thesis: x in omega
then consider a being set  such that
A4: ( a in dom phi & x = phi . a ) by FUNCT_1:def_3;
reconsider a = a as Element of omega by A2, A4;
 x = n |^|^ a by A2, A4;
hence  x in omega by ORDINAL1:def_12; ::_thesis: verum
end;
A5: n |^|^ omega = lim phi by A2, Th15;
now__::_thesis:_(_{}_<>_omega_&_(_for_b,_c_being_ordinal_number_st_b_in_omega_&_omega_in_c_holds_
ex_D_being_Ordinal_st_
(_D_in_dom_phi_&_(_for_E_being_Ordinal_st_D_c=_E_&_E_in_dom_phi_holds_
(_b_in_phi_._E_&_phi_._E_in_c_)_)_)_)_)
thus  {} <> omega ; ::_thesis: for b, c being ordinal number st b in omega & omega in c holds
ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )
let b, c be ordinal number ; ::_thesis: ( b in omega & omega in c implies ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) ) )
assume A6: ( b in omega & omega in c ) ; ::_thesis: ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )
reconsider x = b as Element of omega by A6;
take D = n |^|^ x; ::_thesis: ( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )
thus  D in dom phi by A2, ORDINAL1:def_12; ::_thesis: for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c )
 x < D by A1, Th28;
then A7: b in D by NAT_1:44;
let E be Ordinal; ::_thesis: ( D c= E & E in dom phi implies ( b in phi . E & phi . E in c ) )
assume A8: ( D c= E & E in dom phi ) ; ::_thesis: ( b in phi . E & phi . E in c )
then reconsider e = E as Element of omega by A2;
 ( x < e & e < n |^|^ e ) by A1, Th28, A7, A8, NAT_1:44;
then A9: ( x < n |^|^ e & phi . e = H1(e) ) by A2, XXREAL_0:2;
 phi . E in rng phi by A8, FUNCT_1:def_3;
hence  ( b in phi . E & phi . E in c ) by A6, A9, A3, NAT_1:44, ORDINAL1:10; ::_thesis: verum
end;
then  omega is_limes_of phi by ORDINAL2:def_9;
hence  n |^|^ omega = omega by A5, ORDINAL2:def_10; ::_thesis: verum
end;

theorem Th30: :: ORDINAL5:30
for a being ordinal number st 1 in a holds
a |^|^ omega is limit_ordinal
proof
let a be ordinal number ; ::_thesis: ( 1 in a implies a |^|^ omega is limit_ordinal )
assume A1: 1 in a ; ::_thesis: a |^|^ omega is limit_ordinal
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A2: ( dom phi = omega & ( for b being ordinal number st b in omega holds
phi . b = H1(b) ) ) from ORDINAL2:sch_3();
 phi is increasing
proof
let b be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not b in b1 or not b1 in dom phi or phi . b in phi . b1 )
let c be ordinal number ; ::_thesis: ( not b in c or not c in dom phi or phi . b in phi . c )
assume A3: ( b in c & c in dom phi ) ; ::_thesis: phi . b in phi . c
then reconsider b = b, c = c as Element of NAT by A2, ORDINAL1:10;
 b < c by A3, NAT_1:44;
then  ( phi . b = H1(b) & H1(b) in H1(c) ) by A1, A2, Th24;
hence  phi . b in phi . c by A2; ::_thesis: verum
end;
then  ( lim phi = sup phi & sup phi is limit_ordinal ) by A2, ORDINAL4:8, ORDINAL4:16;
hence  a |^|^ omega is limit_ordinal by A2, Th15; ::_thesis: verum
end;

theorem Th31: :: ORDINAL5:31
for a being ordinal number st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega
proof
let a be ordinal number ; ::_thesis: ( 0 in a implies exp (a,(a |^|^ omega)) = a |^|^ omega )
assume  0 in a ; ::_thesis: exp (a,(a |^|^ omega)) = a |^|^ omega
then  ( 1 = succ 0 & succ 0 c= a ) by ORDINAL1:21;
then A1: ( 1 = a or 1 c< a ) by XBOOLE_0:def_8;
percases ( a = 1 or 1 in a ) by A1, ORDINAL1:11;
supposeA2: a = 1 ; ::_thesis: exp (a,(a |^|^ omega)) = a |^|^ omega
hence  exp (a,(a |^|^ omega)) = 1 by ORDINAL2:46
.= a |^|^ omega by A2, Th17 ;
::_thesis: verum
end;
supposeA3: 1 in a ; ::_thesis: exp (a,(a |^|^ omega)) = a |^|^ omega
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
deffunc H2( Ordinal) ->  set = exp (a,$1);
consider T being Ordinal-Sequence such that
A4: ( dom T = omega & ( for a being ordinal number st a in omega holds
T . a = H1(a) ) ) from ORDINAL2:sch_3();
consider E being Ordinal-Sequence such that
A5: ( dom E = a |^|^ omega & ( for b being ordinal number st b in a |^|^ omega holds
E . b = H2(b) ) ) from ORDINAL2:sch_3();
 0 in 1 by NAT_1:44;
then  ( 0 in a & 0 in omega ) by A3, ORDINAL1:10;
then B6: a c= a |^|^ omega by Th23;
 E is increasing Ordinal-Sequence by A3, A5, ORDINAL4:25;
then  ( lim E = exp (a,(a |^|^ omega)) & Union E is_limes_of E ) by A5, B6, Th6, ORDINAL2:45, A3, Th30;
then A7: exp (a,(a |^|^ omega)) = Union E by ORDINAL2:def_10;
 T is increasing Ordinal-Sequence by A3, A4, Th25;
then  ( lim T = a |^|^ omega & Union T is_limes_of T ) by A4, Th15, Th6;
then A8: a |^|^ omega = Union T by ORDINAL2:def_10;
thus  exp (a,(a |^|^ omega)) c= a |^|^ omega :: according to XBOOLE_0:def_10 ::_thesis: a |^|^ omega c= exp (a,(a |^|^ omega))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in exp (a,(a |^|^ omega)) or x in a |^|^ omega )
assume  x in exp (a,(a |^|^ omega)) ; ::_thesis: x in a |^|^ omega
then consider b being set  such that
A9: ( b in dom E & x in E . b ) by A7, CARD_5:2;
consider c being set  such that
A10: ( c in dom T & b in T . c ) by A5, A8, A9, CARD_5:2;
reconsider b = b as Ordinal by A9;
reconsider c = c as Element of omega by A4, A10;
A11: exp (a,b) in exp (a,(T . c)) by A3, A10, ORDINAL4:24;
A12: succ c in omega by ORDINAL1:28;
then  ( E . b = H2(b) & T . c = H1(c) & T . (succ c) = H1( succ c) ) by A9, A4, A5;
then  E . b in T . (succ c) by A11, Th14;
then  x in T . (succ c) by A9, ORDINAL1:10;
hence  x in a |^|^ omega by A4, A8, A12, CARD_5:2; ::_thesis: verum
end;
thus  a |^|^ omega c= exp (a,(a |^|^ omega)) by A3, ORDINAL4:32; ::_thesis: verum
end;
end;
end;

theorem :: ORDINAL5:32
for a, b being ordinal number st 0 in a & omega c= b holds
a |^|^ b = a |^|^ omega
proof
let a, b be ordinal number ; ::_thesis: ( 0 in a & omega c= b implies a |^|^ b = a |^|^ omega )
assume A1: 0 in a ; ::_thesis: ( not omega c= b or a |^|^ b = a |^|^ omega )
assume  omega c= b ; ::_thesis: a |^|^ b = a |^|^ omega
then A2: b = omega +^ (b -^ omega) by ORDINAL3:def_5;
defpred S1[ Ordinal] means a |^|^ (omega +^ $1) = a |^|^ omega;
A3: S1[ {} ] by ORDINAL2:27;
A4: for c being ordinal number st S1[c] holds
S1[ succ c]
proof
let c be ordinal number ; ::_thesis: ( S1[c] implies S1[ succ c] )
assume  S1[c] ; ::_thesis: S1[ succ c]
then A5: exp (a,(a |^|^ (omega +^ c))) = a |^|^ omega by A1, Th31;
thus a |^|^ (omega +^ (succ c)) = a |^|^ (succ (omega +^ c)) by ORDINAL2:28
.= a |^|^ omega by A5, Th14 ; ::_thesis: verum
end;
A6: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) holds
S1[c]
proof
let c be ordinal number ; ::_thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) implies S1[c] )
assume A7: ( c <> {} & c is limit_ordinal ) ; ::_thesis: ( ex b being ordinal number st
( b in c & not S1[b] ) or S1[c] )
assume A8: for b being ordinal number st b in c holds
S1[b] ; ::_thesis: S1[c]
deffunc H1( Ordinal) ->  Ordinal = a |^|^ $1;
consider f being Ordinal-Sequence such that
A9: ( dom f = omega +^ c & ( for b being ordinal number st b in omega +^ c holds
f . b = H1(b) ) ) from ORDINAL2:sch_3();
 ( omega +^ c <> {} & omega +^ c is limit_ordinal ) by A7, ORDINAL3:26, ORDINAL3:29;
then A10: a |^|^ (omega +^ c) = lim f by A9, Th15;
now__::_thesis:_(_a_|^|^_omega_<>_{}_&_(_for_B,_C_being_Ordinal_st_B_in_a_|^|^_omega_&_a_|^|^_omega_in_C_holds_
ex_D_being_set_st_
(_D_in_dom_f_&_(_for_E_being_Ordinal_st_D_c=_E_&_E_in_dom_f_holds_
(_B_in_f_._E_&_f_._E_in_C_)_)_)_)_)
 a c= a |^|^ omega by A1, Th23;
hence  a |^|^ omega <> {} by A1; ::_thesis: for B, C being Ordinal st B in a |^|^ omega & a |^|^ omega in C holds
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
let B, C be Ordinal; ::_thesis: ( B in a |^|^ omega & a |^|^ omega in C implies ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) ) )
assume A11: ( B in a |^|^ omega & a |^|^ omega in C ) ; ::_thesis: ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
take D = omega ; ::_thesis: ( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
 ( omega +^ {} = omega & {} in c ) by A7, ORDINAL2:27, ORDINAL3:8;
hence  D in dom f by A9, ORDINAL2:32; ::_thesis: for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C )
let E be Ordinal; ::_thesis: ( D c= E & E in dom f implies ( B in f . E & f . E in C ) )
assume A12: ( D c= E & E in dom f ) ; ::_thesis: ( B in f . E & f . E in C )
then  E -^ D in (omega +^ c) -^ omega by A9, ORDINAL3:53;
then  E -^ D in c by ORDINAL3:52;
then  S1[E -^ D] by A8;
then  a |^|^ omega = a |^|^ E by A12, ORDINAL3:def_5;
hence  ( B in f . E & f . E in C ) by A9, A11, A12; ::_thesis: verum
end;
then  a |^|^ omega is_limes_of f by ORDINAL2:def_9;
hence  S1[c] by A10, ORDINAL2:def_10; ::_thesis: verum
end;
 for c being ordinal number holds S1[c] from ORDINAL2:sch_1(A3, A4, A6);
hence  a |^|^ b = a |^|^ omega by A2; ::_thesis: verum
end;

begin

Lm1:  {} in omega
by ORDINAL1:def_11;

scheme :: ORDINAL5:sch 1
CriticalNumber2{ F1() ->  Ordinal, F2() ->  Ordinal-Sequence, F3( Ordinal) ->  Ordinal } :
 ( F1() c= Union F2() & F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
provided
A1: for a, b being ordinal number st a in b holds
F3(a) in F3(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F3(b) ) holds
F3(a) is_limes_of phi and
A3: ( dom F2() = omega & F2() . 0 = F1() ) and
A4: for a being ordinal number st a in omega holds
F2() . (succ a) = F3((F2() . a))
proof
A5: F1() in rng F2() by A3, FUNCT_1:def_3;
hence  F1() c= Union F2() by ZFMISC_1:74; ::_thesis: ( F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
set phi = F2();
A6: now__::_thesis:_for_a_being_ordinal_number_holds_not_S1[a]
defpred S1[ Ordinal] means  not $1 c= F3($1);
assume A7: ex a being ordinal number st S1[a] ; ::_thesis: contradiction
consider a being ordinal number  such that
A8: S1[a] and
A9: for b being ordinal number st S1[b] holds
a c= b from ORDINAL1:sch_1(A7);
 F3(F3(a)) in F3(a) by A1, A8, ORDINAL1:16;
then  not F3(a) c= F3(F3(a)) by ORDINAL1:5;
hence  contradiction by A8, A9; ::_thesis: verum
end;
then  F1() c= F3(F1()) ;
then A10: ( F1() c< F3(F1()) or F1() = F3(F1()) ) by XBOOLE_0:def_8;
percases ( F3(F1()) = F1() or F1() in F3(F1()) ) by A10, ORDINAL1:11;
supposeA11: F3(F1()) = F1() ; ::_thesis: ( F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
A12: for a being set st a in omega holds
F2() . a = F1()
proof
let a be set ; ::_thesis: ( a in omega implies F2() . a = F1() )
assume  a in omega ; ::_thesis: F2() . a = F1()
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means F2() . $1 = F1();
A13: S1[ 0 ] by A3;
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]
 n in omega by ORDINAL1:def_12;
then  F2() . (succ n) = F3(F1()) by A4, A15;
hence  S1[n + 1] by A11, NAT_1:38; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A13, A14);
then  S1[a] ;
hence  F2() . a = F1() ; ::_thesis: verum
end;
 rng F2() = {F1()}
proof
thus  rng F2() c= {F1()} :: according to XBOOLE_0:def_10 ::_thesis: {F1()} c= rng F2()
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F2() or x in {F1()} )
assume  x in rng F2() ; ::_thesis: x in {F1()}
then consider a being set  such that
A16: ( a in dom F2() & x = F2() . a ) by FUNCT_1:def_3;
 x = F1() by A12, A16, A3;
hence  x in {F1()} by TARSKI:def_1; ::_thesis: verum
end;
thus  {F1()} c= rng F2() by A5, ZFMISC_1:31; ::_thesis: verum
end;
then  Union F2() = F1() by ZFMISC_1:25;
hence  ( F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) ) by A11; ::_thesis: verum
end;
supposeA17: F1() in F3(F1()) ; ::_thesis: ( F3((Union F2())) = Union F2() & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
deffunc H1( Ordinal, Ordinal) ->  Ordinal = F3($2);
deffunc H2( Ordinal, T-Sequence) ->  set = {} ;
A18: now__::_thesis:_for_a_being_ordinal_number_st_succ_a_in_omega_holds_
F2()_._(succ_a)_=_H1(a,F2()_._a)
let a be ordinal number ; ::_thesis: ( succ a in omega implies F2() . (succ a) = H1(a,F2() . a) )
assume A19: succ a in omega ; ::_thesis: F2() . (succ a) = H1(a,F2() . a)
 a in succ a by ORDINAL1:6;
hence  F2() . (succ a) = H1(a,F2() . a) by A4, A19, ORDINAL1:10; ::_thesis: verum
end;
A20: for a being ordinal number st a in omega holds
( F1() c= F2() . a & F2() . a in F2() . (succ a) )
proof
let a be ordinal number ; ::_thesis: ( a in omega implies ( F1() c= F2() . a & F2() . a in F2() . (succ a) ) )
assume  a in omega ; ::_thesis: ( F1() c= F2() . a & F2() . a in F2() . (succ a) )
then reconsider a = a as Element of omega ;
defpred S1[ Nat] means ( F1() c= F2() . $1 & F2() . $1 in F2() . (succ $1) );
A21: S1[ 0 ] by A17, A3, A4;
A22: 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 A23: S1[n] ; ::_thesis: S1[n + 1]
A24: ( n + 1 = succ n & (n + 1) + 1 = succ (n + 1) & n + 1 in omega & (n + 1) + 1 in omega ) by NAT_1:38;
then  ( F2() . (n + 1) = F3((F2() . n)) & F2() . ((n + 1) + 1) = F3((F2() . (n + 1))) ) by A18;
then  ( F2() . n c= F2() . (n + 1) & F2() . (n + 1) in F2() . ((n + 1) + 1) ) by A1, A6, A23, A24;
hence  S1[n + 1] by A23, NAT_1:38, XBOOLE_1:1; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A21, A22);
then  S1[a] ;
hence  ( F1() c= F2() . a & F2() . a in F2() . (succ a) ) ; ::_thesis: verum
end;
deffunc H3( Ordinal) ->  Ordinal = F3($1);
consider fi being Ordinal-Sequence such that
A25: ( dom fi = Union F2() & ( for a being ordinal number st a in Union F2() holds
fi . a = H3(a) ) ) from ORDINAL2:sch_3();
 1 = succ 0 ;
then  F2() . 1 = H3(F1()) by A3, A4;
then  H3(F1()) in rng F2() by A3, FUNCT_1:def_3;
then B26: H3(F1()) c= Union F2() by ZFMISC_1:74;
now__::_thesis:_for_c_being_ordinal_number_st_c_in_Union_F2()_holds_
succ_c_in_Union_F2()
let c be ordinal number ; ::_thesis: ( c in Union F2() implies succ c in Union F2() )
assume  c in Union F2() ; ::_thesis: succ c in Union F2()
then consider x being set  such that
A27: ( x in dom F2() & c in F2() . x ) by CARD_5:2;
reconsider x = x as Element of omega by A3, A27;
 ( succ c c= F2() . x & F2() . x in F2() . (succ x) ) by A20, A27, ORDINAL1:21;
then  ( succ c in F2() . (succ x) & succ x in omega ) by ORDINAL1:12, ORDINAL1:def_12;
hence  succ c in Union F2() by A3, CARD_5:2; ::_thesis: verum
end;
then A28: Union F2() is limit_ordinal by ORDINAL1:28;
then A29: H3( Union F2()) is_limes_of fi by A2, A25, B26, A17;
 fi is increasing
proof
let a be ordinal number ; :: 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 number ; ::_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 A25, ORDINAL1:10;
hence  fi . a in fi . b by A1, A30; ::_thesis: verum
end;
then A31: sup fi = lim fi by A25, B26, A28, ORDINAL4:8, A17
.= H3( Union F2()) by A29, ORDINAL2:def_10 ;
thus  H3( Union F2()) c= Union F2() :: according to XBOOLE_0:def_10 ::_thesis: ( Union F2() c= F3((Union F2())) & ( for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b ) )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in H3( Union F2()) or x in Union F2() )
assume A32: x in H3( Union F2()) ; ::_thesis: x in Union F2()
then reconsider A = x as Ordinal ;
consider b being ordinal number  such that
A33: ( b in rng fi & A c= b ) by A31, A32, ORDINAL2:21;
consider y being set  such that
A34: ( y in dom fi & b = fi . y ) by A33, FUNCT_1:def_3;
reconsider y = y as Ordinal by A34;
consider z being set  such that
A35: ( z in dom F2() & y in F2() . z ) by A25, A34, CARD_5:2;
reconsider z = z as Ordinal by A35;
set c = F2() . z;
 succ z in omega by A3, A35, ORDINAL1:28;
then  ( F2() . (succ z) = H3(F2() . z) & F2() . (succ z) in rng F2() & b = H3(y) ) by A3, A18, A25, A34, FUNCT_1:def_3;
then  ( b in H3(F2() . z) & H3(F2() . z) c= Union F2() ) by A1, A35, ZFMISC_1:74;
hence  x in Union F2() by A33, ORDINAL1:12; ::_thesis: verum
end;
thus  Union F2() c= H3( Union F2()) by A6; ::_thesis: for b being ordinal number st F1() c= b & F3(b) = b holds
Union F2() c= b
let b be ordinal number ; ::_thesis: ( F1() c= b & F3(b) = b implies Union F2() c= b )
assume A36: ( F1() c= b & H3(b) = b ) ; ::_thesis: Union F2() c= b
 rng F2() c= b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F2() or x in b )
assume  x in rng F2() ; ::_thesis: x in b
then consider a being set  such that
A37: ( a in dom F2() & x = F2() . a ) by FUNCT_1:def_3;
reconsider a = a as Element of omega by A3, A37;
defpred S1[ Nat] means F2() . $1 in b;
 F1() <> b by A17, A36;
then  F1() c< b by A36, XBOOLE_0:def_8;
then A38: S1[ 0 ] by A3, ORDINAL1:11;
A39: 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  S1[n] ; ::_thesis: S1[n + 1]
then  ( H3(F2() . n) in b & n in omega ) by A1, A36, ORDINAL1:def_12;
then  F2() . (succ n) in b by A4;
hence  S1[n + 1] by NAT_1:38; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A38, A39);
then  S1[a] ;
hence  x in b by A37; ::_thesis: verum
end;
then  ( Union F2() c= union b & union b c= b ) by ORDINAL2:5, ZFMISC_1:77;
hence  Union F2() c= b by XBOOLE_1:1; ::_thesis: verum
end;
end;
end;

scheme :: ORDINAL5:sch 2
CriticalNumber3{ F1() ->  Ordinal, F2( Ordinal) ->  Ordinal } :
 ex a being ordinal number st
( F1() in a & F2(a) = a )
provided
A1: for a, b being ordinal number st a in b holds
F2(a) in F2(b) and
A2: for a being ordinal number st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = F2(b) ) holds
F2(a) is_limes_of phi
proof
assume A3: for a being ordinal number holds
( not F1() in a or not F2(a) = a ) ; ::_thesis: contradiction
deffunc H1( Ordinal, Ordinal) ->  Ordinal = F2($2);
deffunc H2( Ordinal, T-Sequence) ->  set = {} ;
consider phi being Ordinal-Sequence such that
A4: dom phi = omega and
A5: ( {} in omega implies phi . {} = succ F1() ) and
A6: for a being ordinal number st succ a in omega holds
phi . (succ a) = H1(a,phi . a) and
 for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
phi . a = H2(a,phi | a) from ORDINAL2:sch_11();
A7: now__::_thesis:_for_a_being_ordinal_number_holds_not_S1[a]
defpred S1[ Ordinal] means  not $1 c= F2($1);
assume A8: ex a being ordinal number st S1[a] ; ::_thesis: contradiction
consider a being ordinal number  such that
A9: S1[a] and
A10: for b being ordinal number 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_number_st_F1()_in_a_holds_
a_in_F2(a)
let a be ordinal number ; ::_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) by XBOOLE_0:def_8;
hence  a in F2(a) by ORDINAL1:11; ::_thesis: verum
end;
A12: for a being ordinal number st a in omega holds
F1() in phi . a
proof
let a be ordinal number ; ::_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]
 ( n + 1 = succ 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 number ; :: 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 number ; ::_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 number 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[ {} ] ;
A20: for c being ordinal number st S1[c] holds
S1[ succ c]
proof
let c be ordinal number ; ::_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 number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A25: ( 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
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 number 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 number 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, Lm1, 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 number ; :: 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 number ; ::_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 set ; :: according to TARSKI:def_3 ::_thesis: ( not x in sup fi or x in sup phi )
assume A33: x in sup fi ; ::_thesis: x in sup phi
then reconsider A = x as Ordinal ;
consider b being ordinal number  such that
A34: ( b in rng fi & A c= b ) by A33, ORDINAL2:21;
consider y being set  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 number  such that
A36: ( c in rng phi & y c= c ) by A27, A35, ORDINAL2:21;
consider z being set  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 ) ) by XBOOLE_0:def_8;
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
end;

begin

definition
let a be ordinal number ;
attra is epsilon  means :Def5: :: ORDINAL5:def 5
 exp (omega,a) = a;
end;

:: deftheorem Def5 defines epsilon ORDINAL5:def_5_:_
 for a being ordinal number holds
( a is epsilon iff exp (omega,a) = a );

theorem Th33: :: ORDINAL5:33
for a being ordinal number ex b being ordinal number st
( a in b & b is epsilon )
proof
let a be ordinal number ; ::_thesis: ex b being ordinal number st
( a in b & b is epsilon )
deffunc H1( Ordinal) ->  set = exp (omega,$1);
A1: for a, b being ordinal number st a in b holds
H1(a) in H1(b) by ORDINAL4:24;
A2: now__::_thesis:_for_a_being_ordinal_number_st_not_a_is_empty_&_a_is_limit_ordinal_holds_
for_phi_being_Ordinal-Sequence_st_dom_phi_=_a_&_(_for_b_being_ordinal_number_st_b_in_a_holds_
phi_._b_=_H1(b)_)_holds_
H1(a)_is_limes_of_phi
let a be ordinal number ; ::_thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi )
assume A3: ( not a is empty & a is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi
let phi be Ordinal-Sequence; ::_thesis: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) implies H1(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) ) ; ::_thesis: H1(a) is_limes_of phi
 phi is non-decreasing
proof
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st b in b & b in dom phi holds
phi . b c= phi . b
let c be ordinal number ; ::_thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume A5: ( b in c & c in dom phi ) ; ::_thesis: phi . b c= phi . c
then  ( phi . b = H1(b) & phi . c = H1(c) ) by A4, ORDINAL1:10;
then  phi . b in phi . c by A5, ORDINAL4:24;
hence  phi . b c= phi . c by ORDINAL1:def_2; ::_thesis: verum
end;
then  ( Union phi is_limes_of phi & H1(a) = lim phi ) by A3, A4, Th6, ORDINAL2:45;
hence  H1(a) is_limes_of phi by ORDINAL2:def_10; ::_thesis: verum
end;
consider b being ordinal number  such that
A6: ( a in b & H1(b) = b ) from ORDINAL5:sch_2(A1, A2);
take  b ; ::_thesis: ( a in b & b is epsilon )
thus  a in b by A6; ::_thesis: b is epsilon
thus  exp (omega,b) = b by A6; :: according to ORDINAL5:def_5 ::_thesis: verum
end;

registration
cluster epsilon-transitive epsilon-connected ordinal epsilon for set ;
existence
 ex b1 being ordinal number st b1 is epsilon
proof
 ex a being ordinal number st
( 0 in a & a is epsilon ) by Th33;
hence  ex b1 being ordinal number st b1 is epsilon ; ::_thesis: verum
end;
end;

definition
let a be Ordinal;
func first_epsilon_greater_than a ->  epsilon Ordinal means :Def6: :: ORDINAL5:def 6
( a in it & ( for b being epsilon Ordinal st a in b holds
it c= b ) );
existence
 ex b1 being epsilon Ordinal st
( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) )
proof
defpred S1[ Ordinal] means ( a in $1 & $1 is epsilon );
A1: ex c being ordinal number st S1[c] by Th33;
consider c being ordinal number  such that
A2: ( S1[c] & ( for b being ordinal number st S1[b] holds
c c= b ) ) from ORDINAL1:sch_1(A1);
reconsider c = c as epsilon Ordinal by A2;
take  c ; ::_thesis: ( a in c & ( for b being epsilon Ordinal st a in b holds
c c= b ) )
thus  ( a in c & ( for b being epsilon Ordinal st a in b holds
c c= b ) ) by A2; ::_thesis: verum
end;
uniqueness
 for b1, b2 being epsilon Ordinal st a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) & a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) holds
b1 = b2
proof
let b1, b2 be epsilon Ordinal; ::_thesis: ( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) & a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) implies b1 = b2 )
assume that
A3: ( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) ) and
A4: ( a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) ) ; ::_thesis: b1 = b2
thus  ( b1 c= b2 & b2 c= b1 ) by A3, A4; :: according to XBOOLE_0:def_10 ::_thesis: verum
end;
end;

:: deftheorem Def6 defines first_epsilon_greater_than ORDINAL5:def_6_:_
 for a being Ordinal
for b2 being epsilon Ordinal holds
( b2 = first_epsilon_greater_than a iff ( a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) ) );

theorem :: ORDINAL5:34
for a, b being ordinal number st a c= b holds
first_epsilon_greater_than a c= first_epsilon_greater_than b
proof
let a, b be ordinal number ; ::_thesis: ( a c= b implies first_epsilon_greater_than a c= first_epsilon_greater_than b )
assume A1: a c= b ; ::_thesis: first_epsilon_greater_than a c= first_epsilon_greater_than b
 b in first_epsilon_greater_than b by Def6;
then  a in first_epsilon_greater_than b by A1, ORDINAL1:12;
hence  first_epsilon_greater_than a c= first_epsilon_greater_than b by Def6; ::_thesis: verum
end;

theorem :: ORDINAL5:35
for a, b being ordinal number st a in b & b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a
proof
let a, b be ordinal number ; ::_thesis: ( a in b & b in first_epsilon_greater_than a implies first_epsilon_greater_than b = first_epsilon_greater_than a )
assume A1: ( a in b & b in first_epsilon_greater_than a ) ; ::_thesis: first_epsilon_greater_than b = first_epsilon_greater_than a
now__::_thesis:_for_c_being_epsilon_Ordinal_st_b_in_c_holds_
first_epsilon_greater_than_a_c=_c
let c be epsilon Ordinal; ::_thesis: ( b in c implies first_epsilon_greater_than a c= c )
assume  b in c ; ::_thesis: first_epsilon_greater_than a c= c
then  a in c by A1, ORDINAL1:10;
hence  first_epsilon_greater_than a c= c by Def6; ::_thesis: verum
end;
hence  first_epsilon_greater_than b = first_epsilon_greater_than a by A1, Def6; ::_thesis: verum
end;

theorem Th36: :: ORDINAL5:36
first_epsilon_greater_than 0 = omega |^|^ omega
proof
deffunc H1( Ordinal) ->  set = exp (omega,$1);
A1: for a, b being ordinal number st a in b holds
H1(a) in H1(b) by ORDINAL4:24;
A2: now__::_thesis:_for_a_being_ordinal_number_st_not_a_is_empty_&_a_is_limit_ordinal_holds_
for_phi_being_Ordinal-Sequence_st_dom_phi_=_a_&_(_for_b_being_ordinal_number_st_b_in_a_holds_
phi_._b_=_H1(b)_)_holds_
H1(a)_is_limes_of_phi
let a be ordinal number ; ::_thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi )
assume A3: ( not a is empty & a is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi
let phi be Ordinal-Sequence; ::_thesis: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) implies H1(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) ) ; ::_thesis: H1(a) is_limes_of phi
 phi is non-decreasing
proof
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st b in b & b in dom phi holds
phi . b c= phi . b
let c be ordinal number ; ::_thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume A5: ( b in c & c in dom phi ) ; ::_thesis: phi . b c= phi . c
then  ( phi . b = H1(b) & phi . c = H1(c) ) by A4, ORDINAL1:10;
then  phi . b in phi . c by A5, ORDINAL4:24;
hence  phi . b c= phi . c by ORDINAL1:def_2; ::_thesis: verum
end;
then  ( Union phi is_limes_of phi & H1(a) = lim phi ) by A3, A4, Th6, ORDINAL2:45;
hence  H1(a) is_limes_of phi by ORDINAL2:def_10; ::_thesis: verum
end;
deffunc H2( Ordinal, Ordinal) ->  set = H1($2);
deffunc H3( Ordinal, Ordinal-Sequence) ->  set = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: ( {} in omega implies f . {} = 1 ) and
A8: for a being ordinal number st succ a in omega holds
f . (succ a) = H2(a,f . a) and
 for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
f . a = H3(a,f | a) from ORDINAL2:sch_11();
A9: ( dom f = omega & f . 0 = 1 ) by A6, A7;
A10: now__::_thesis:_for_a_being_ordinal_number_st_a_in_omega_holds_
f_._(succ_a)_=_H1(f_._a)
let a be ordinal number ; ::_thesis: ( a in omega implies f . (succ a) = H1(f . a) )
assume  a in omega ; ::_thesis: f . (succ a) = H1(f . a)
then  succ a in omega by ORDINAL1:28;
hence  f . (succ a) = H1(f . a) by A8; ::_thesis: verum
end;
A11: ( 1 c= Union f & H1( Union f) = Union f & ( for b being ordinal number st 1 c= b & H1(b) = b holds
Union f c= b ) ) from ORDINAL5:sch_1(A1, A2, A9, A10);
 Union f is epsilon
proof
thus  H1( Union f) = Union f by A11; :: according to ORDINAL5:def_5 ::_thesis: verum
end;
then reconsider e = Union f as epsilon Ordinal ;
defpred S1[ Nat] means f . $1 = omega |^|^ $1;
A12: S1[ 0 ] by A7, Th13;
A13: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A14: S1[n] ; ::_thesis: S1[n + 1]
A15: ( n + 1 = succ n & n in omega ) by NAT_1:38, ORDINAL1:def_12;
hence f . (n + 1) = H1(f . n) by A10
.= omega |^|^ (n + 1) by A14, A15, Th14 ;
::_thesis: verum
end;
A16: for n being Nat holds S1[n] from NAT_1:sch_2(A12, A13);
then  for c being ordinal number st c in omega holds
f . c = omega |^|^ c ;
then A17: omega |^|^ omega = lim f by A6, Th15;
 f is non-decreasing
proof
let a be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st a in b & b in dom f holds
f . a c= f . b
let b be ordinal number ; ::_thesis: ( a in b & b in dom f implies f . a c= f . b )
assume A18: ( a in b & b in dom f ) ; ::_thesis: f . a c= f . b
then reconsider n = a, m = b as Element of omega by A6, ORDINAL1:10;
 a c= b by A18, ORDINAL1:def_2;
then  omega |^|^ a c= omega |^|^ b by Th21;
then  f . n c= omega |^|^ m by A16;
hence  f . a c= f . b by A16; ::_thesis: verum
end;
then  e is_limes_of f by A6, Th6;
then A19: omega |^|^ omega = e by A17, ORDINAL2:def_10;
A20: succ 0 = 1 ;
then B21: 0 in 1 by ORDINAL1:6;
now__::_thesis:_for_b_being_epsilon_Ordinal_st_0_in_b_holds_
e_c=_b
let b be epsilon Ordinal; ::_thesis: ( 0 in b implies e c= b )
assume  0 in b ; ::_thesis: e c= b
then  ( 1 c= b & H1(b) = b ) by A20, Def5, ORDINAL1:21;
hence  e c= b by A11; ::_thesis: verum
end;
hence  first_epsilon_greater_than 0 = omega |^|^ omega by A19, B21, Def6, A11; ::_thesis: verum
end;

theorem Th37: :: ORDINAL5:37
for e being epsilon Ordinal holds omega in e
proof
let e be epsilon Ordinal; ::_thesis: omega in e
A1: exp (omega,e) = e by Def5;
A2: ( exp (omega,0) = 1 & exp (omega,1) = omega & 1 in omega ) by ORDINAL2:43, ORDINAL2:46;
then A3: ( e <> 0 & e <> 1 & succ 0 = 1 & succ 1 = 2 ) by Def5;
then  0 in e by ORDINAL3:8;
then  1 c= e by A3, ORDINAL1:21;
then  1 c< e by A3, XBOOLE_0:def_8;
then  1 in e by ORDINAL1:11;
hence  omega in e by A1, A2, ORDINAL4:24; ::_thesis: verum
end;

registration
cluster ordinal epsilon  ->  non empty limit_ordinal for set ;
coherence
 for b1 being Ordinal st b1 is epsilon holds
( not b1 is empty & b1 is limit_ordinal )
proof
let e be Ordinal; ::_thesis: ( e is epsilon implies ( not e is empty & e is limit_ordinal ) )
assume A1: e is epsilon ; ::_thesis: ( not e is empty & e is limit_ordinal )
 exp (omega,0) = 1 by ORDINAL2:43;
hence  not e is empty by A1, Def5; ::_thesis: e is limit_ordinal
then  ( 0 in e & exp (omega,e) = e ) by A1, Def5, ORDINAL3:8;
hence  e is limit_ordinal by Th9; ::_thesis: verum
end;
end;

theorem Th38: :: ORDINAL5:38
for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))
proof
let e be epsilon Ordinal; ::_thesis: exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))
thus  exp (omega,(exp (e,omega))) = exp (omega,(exp (e,(1 +^ omega)))) by CARD_2:74
.= exp (omega,((exp (e,omega)) *^ (exp (e,1)))) by ORDINAL4:30
.= exp (omega,((exp (e,omega)) *^ e)) by ORDINAL2:46
.= exp ((exp (omega,e)),(exp (e,omega))) by ORDINAL4:31
.= exp (e,(exp (e,omega))) by Def5 ; ::_thesis: verum
end;

theorem Th39: :: ORDINAL5:39
for n being Nat
for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
proof
let n be Nat; ::_thesis: for e being epsilon Ordinal st 0 in n holds
e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
let e be epsilon Ordinal; ::_thesis: ( 0 in n implies e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1))) )
assume A1: 0 in n ; ::_thesis: e |^|^ (n + 2) = exp (omega,(e |^|^ (n + 1)))
 0 in e by ORDINAL3:8;
then  ( omega in e & e c= e |^|^ n ) by A1, Th23, Th37;
then A2: omega c= e |^|^ n by ORDINAL1:def_2;
thus e |^|^ (n + 2) = e |^|^ ((n + 1) + 1)
.= e |^|^ (succ (n + 1)) by NAT_1:38
.= exp (e,(e |^|^ (n + 1))) by Th14
.= exp ((exp (omega,e)),(e |^|^ (n + 1))) by Def5
.= exp (omega,((e |^|^ (n + 1)) *^ e)) by ORDINAL4:31
.= exp (omega,((e |^|^ (succ n)) *^ e)) by NAT_1:38
.= exp (omega,((exp (e,(e |^|^ n))) *^ e)) by Th14
.= exp (omega,((exp (e,(e |^|^ n))) *^ (exp (e,1)))) by ORDINAL2:46
.= exp (omega,(exp (e,(1 +^ (e |^|^ n))))) by ORDINAL4:30
.= exp (omega,(exp (e,(e |^|^ n)))) by A2, CARD_2:74
.= exp (omega,(e |^|^ (succ n))) by Th14
.= exp (omega,(e |^|^ (n + 1))) by NAT_1:38 ; ::_thesis: verum
end;

theorem Th40: :: ORDINAL5:40
for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega
proof
let e be epsilon Ordinal; ::_thesis: first_epsilon_greater_than e = e |^|^ omega
deffunc H1( Ordinal) ->  set = exp (omega,$1);
A1: for a, b being ordinal number st a in b holds
H1(a) in H1(b) by ORDINAL4:24;
A2: now__::_thesis:_for_a_being_ordinal_number_st_not_a_is_empty_&_a_is_limit_ordinal_holds_
for_phi_being_Ordinal-Sequence_st_dom_phi_=_a_&_(_for_b_being_ordinal_number_st_b_in_a_holds_
phi_._b_=_H1(b)_)_holds_
H1(a)_is_limes_of_phi
let a be ordinal number ; ::_thesis: ( not a is empty & a is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi )
assume A3: ( not a is empty & a is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) holds
H1(a) is_limes_of phi
let phi be Ordinal-Sequence; ::_thesis: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) implies H1(a) is_limes_of phi )
assume A4: ( dom phi = a & ( for b being ordinal number st b in a holds
phi . b = H1(b) ) ) ; ::_thesis: H1(a) is_limes_of phi
 phi is non-decreasing
proof
let b be ordinal number ; :: according to ORDINAL5:def_2 ::_thesis: for b being ordinal number st b in b & b in dom phi holds
phi . b c= phi . b
let c be ordinal number ; ::_thesis: ( b in c & c in dom phi implies phi . b c= phi . c )
assume A5: ( b in c & c in dom phi ) ; ::_thesis: phi . b c= phi . c
then  ( phi . b = H1(b) & phi . c = H1(c) ) by A4, ORDINAL1:10;
then  phi . b in phi . c by A5, ORDINAL4:24;
hence  phi . b c= phi . c by ORDINAL1:def_2; ::_thesis: verum
end;
then  ( Union phi is_limes_of phi & H1(a) = lim phi ) by A3, A4, Th6, ORDINAL2:45;
hence  H1(a) is_limes_of phi by ORDINAL2:def_10; ::_thesis: verum
end;
deffunc H2( Ordinal, Ordinal) ->  set = H1($2);
deffunc H3( Ordinal, Ordinal-Sequence) ->  set = lim $2;
consider f being Ordinal-Sequence such that
A6: dom f = omega and
A7: ( {} in omega implies f . {} = succ e ) and
A8: for a being ordinal number st succ a in omega holds
f . (succ a) = H2(a,f . a) and
 for a being ordinal number st a in omega & a <> {} & a is limit_ordinal holds
f . a = H3(a,f | a) from ORDINAL2:sch_11();
A9: ( dom f = omega & f . 0 = succ e ) by A6, A7;
A10: now__::_thesis:_for_a_being_ordinal_number_st_a_in_omega_holds_
f_._(succ_a)_=_H1(f_._a)
let a be ordinal number ; ::_thesis: ( a in omega implies f . (succ a) = H1(f . a) )
assume  a in omega ; ::_thesis: f . (succ a) = H1(f . a)
then  succ a in omega by ORDINAL1:28;
hence  f . (succ a) = H1(f . a) by A8; ::_thesis: verum
end;
A11: ( succ e c= Union f & H1( Union f) = Union f & ( for b being ordinal number st succ e c= b & H1(b) = b holds
Union f c= b ) ) from ORDINAL5:sch_1(A1, A2, A9, A10);
 Union f is epsilon
proof
thus  H1( Union f) = Union f by A11; :: according to ORDINAL5:def_5 ::_thesis: verum
end;
then reconsider e9 = Union f as epsilon Ordinal ;
B12: now__::_thesis:_(_e_in_e9_&_(_for_b_being_epsilon_Ordinal_st_e_in_b_holds_
e9_c=_b_)_)
 e in succ e by ORDINAL1:6;
hence  e in e9 by A11; ::_thesis: for b being epsilon Ordinal st e in b holds
e9 c= b
let b be epsilon Ordinal; ::_thesis: ( e in b implies e9 c= b )
assume  e in b ; ::_thesis: e9 c= b
then  ( succ e c= b & H1(b) = b ) by Def5, ORDINAL1:21;
hence  e9 c= b by A11; ::_thesis: verum
end;
A13: ( succ 0 = 1 & succ 1 = 2 & succ 2 = 3 ) ;
then A14: f . 1 = H1( succ e) by A7, A8
.= omega *^ H1(e) by ORDINAL2:44
.= omega *^ e by Def5 ;
then A15: f . 2 = H1(omega *^ e) by A13, A8
.= exp (H1(e),omega) by ORDINAL4:31
.= exp (e,omega) by Def5 ;
then A16: f . 3 = H1( exp (e,omega)) by A13, A8
.= exp (e,(exp (e,omega))) by Th38 ;
A17: ( e |^|^ 0 = 1 & e |^|^ 1 = e & e |^|^ 2 = exp (e,e) ) by Th13, Th16, Th18;
 ( omega in e & 1 in omega ) by Th37;
then A18: 1 in e by ORDINAL1:10;
then  ( exp (e,1) in exp (e,e) & exp (e,1) in exp (e,omega) ) by ORDINAL4:24;
then A19: ( e in exp (e,e) & e in exp (e,omega) ) by ORDINAL2:46;
defpred S1[ Nat] means ( e |^|^ $1 in f . ($1 + 1) & f . $1 in e |^|^ ($1 + 2) );
 ( e in exp (e,e) & exp (e,e) is limit_ordinal ) by A17, A18, Th24, Th9, ORDINAL3:8;
then A20: S1[ 0 ] by A7, A14, A17, ORDINAL1:28, ORDINAL3:32;
A21: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A22: S1[n] ; ::_thesis: S1[n + 1]
A23: ( n + 1 = succ n & (n + 1) + 1 = succ (n + 1) & n in omega & n + 1 in omega ) by NAT_1:38, ORDINAL1:def_12;
then A24: ( f . (n + 1) = H1(f . n) & f . ((n + 1) + 1) = H1(f . (n + 1)) ) by A10;
thus  e |^|^ (n + 1) in f . ((n + 1) + 1) ::_thesis: f . (n + 1) in e |^|^ ((n + 1) + 2)
proof
percases ( n = 0 or n = 1 or n >= 2 ) by NAT_1:23;
suppose n = 0 ; ::_thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)
hence  e |^|^ (n + 1) in f . ((n + 1) + 1) by A15, Th16, A19; ::_thesis: verum
end;
suppose n = 1 ; ::_thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)
hence  e |^|^ (n + 1) in f . ((n + 1) + 1) by A16, A17, A18, A19, ORDINAL4:24; ::_thesis: verum
end;
suppose n >= 2 ; ::_thesis: e |^|^ (n + 1) in f . ((n + 1) + 1)
then consider k being Nat such that
A25: n = 2 + k by NAT_1:10;
 ( 0 in k + 1 & k + 2 = (k + 1) + 1 ) by NAT_1:44;
then  H1(e |^|^ (k + 2)) = e |^|^ ((k + 1) + 2) by Th39;
hence  e |^|^ (n + 1) in f . ((n + 1) + 1) by A24, A25, A22, ORDINAL4:24; ::_thesis: verum
end;
end;
end;
 ( 0 in n + 1 & n + 2 = (n + 1) + 1 ) by NAT_1:44;
then  H1(e |^|^ (n + 2)) = e |^|^ ((n + 1) + 2) by Th39;
then  H1(f . n) in e |^|^ ((n + 1) + 2) by A22, ORDINAL4:24;
hence  f . (n + 1) in e |^|^ ((n + 1) + 2) by A23, A10; ::_thesis: verum
end;
A26: for n being Nat holds S1[n] from NAT_1:sch_2(A20, A21);
deffunc H4( Ordinal) ->  Ordinal = e |^|^ $1;
consider g being Ordinal-Sequence such that
A27: ( dom g = omega & ( for a being ordinal number st a in omega holds
g . a = H4(a) ) ) from ORDINAL2:sch_3();
A28: e |^|^ omega = lim g by A27, Th15;
 ( 1 in omega & omega in e ) by Th37;
then  1 in e by ORDINAL1:10;
then  g is increasing Ordinal-Sequence by A27, Th25;
then  Union g is_limes_of g by A27, Th6;
then A29: e |^|^ omega = Union g by A28, ORDINAL2:def_10;
 e9 = Union g
proof
thus  e9 c= Union g :: according to XBOOLE_0:def_10 ::_thesis: Union g c= e9
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in e9 or x in Union g )
assume  x in e9 ; ::_thesis: x in Union g
then consider a being set  such that
A30: ( a in dom f & x in f . a ) by CARD_5:2;
reconsider a = a as Element of omega by A6, A30;
 ( f . a in e |^|^ (a + 2) & g . (a + 2) = H4(a + 2) ) by A26, A27;
then  f . a in Union g by A27, CARD_5:2;
hence  x in Union g by A30, ORDINAL1:10; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union g or x in e9 )
assume  x in Union g ; ::_thesis: x in e9
then consider a being set  such that
A31: ( a in dom g & x in g . a ) by CARD_5:2;
reconsider a = a as Element of omega by A27, A31;
 ( a + 1 in omega & e |^|^ a in f . (a + 1) & g . a = H4(a) ) by A26, A27;
then  g . a in Union f by A6, CARD_5:2;
hence  x in e9 by A31, ORDINAL1:10; ::_thesis: verum
end;
hence  first_epsilon_greater_than e = e |^|^ omega by B12, A29, Def6; ::_thesis: verum
end;

definition
let a be Ordinal;
func epsilon_ a ->  Ordinal means :Def7: :: ORDINAL5:def 7
 ex phi being Ordinal-Sequence st
( it = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
correctness
existence
ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) );
uniqueness
for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal) ->  Ordinal = $2 |^|^ omega;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
 ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ a & fi . {} = omega |^|^ omega & ( for c being Ordinal st succ c in succ a holds
fi . (succ c) = H1(c,fi . c) ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ a & fi . {} = omega |^|^ omega & ( for C being Ordinal st succ C in succ a holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ a & fi . {} = omega |^|^ omega & ( for C being Ordinal st succ C in succ a holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ a & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
hence  ( ex b1 being Ordinal ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ( for b1, b2 being Ordinal st ex phi being Ordinal-Sequence st
( b1 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) & ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2 ) ) ; ::_thesis: verum
end;
end;

:: deftheorem Def7 defines epsilon_ ORDINAL5:def_7_:_
 for a, b2 being Ordinal holds
( b2 = epsilon_ a iff ex phi being Ordinal-Sequence st
( b2 = last phi & dom phi = succ a & phi . {} = omega |^|^ omega & ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) & ( for c being Ordinal st c in succ a & c <> {} & c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th41: :: ORDINAL5:41
epsilon_ 0 = omega |^|^ omega
proof
deffunc H1( Ordinal) ->  Ordinal = epsilon_ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  Ordinal = $2 |^|^ omega;
A1: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = omega |^|^ omega & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def7;
thus  H1( 0 ) = omega |^|^ omega from ORDINAL2:sch_14(A1); ::_thesis: verum
end;

theorem Th42: :: ORDINAL5:42
for a being ordinal number holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega
proof
let a be ordinal number ; ::_thesis: epsilon_ (succ a) = (epsilon_ a) |^|^ omega
deffunc H1( Ordinal) ->  Ordinal = epsilon_ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  Ordinal = $2 |^|^ omega;
A1: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = omega |^|^ omega & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def7;
 for b being ordinal number holds H1( succ b) = H3(b,H1(b)) from ORDINAL2:sch_15(A1);
hence  epsilon_ (succ a) = (epsilon_ a) |^|^ omega ; ::_thesis: verum
end;

theorem Th43: :: ORDINAL5:43
for b being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi )
assume A1: ( b <> {} & b is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi
deffunc H1( Ordinal) ->  Ordinal = epsilon_ $1;
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = lim $2;
deffunc H3( Ordinal, Ordinal) ->  Ordinal = $2 |^|^ omega;
let fi be Ordinal-Sequence; ::_thesis: ( dom fi = b & ( for c being ordinal number st c in b holds
fi . c = epsilon_ c ) implies epsilon_ b = lim fi )
assume that
A2: dom fi = b and
A3: for c being ordinal number st c in b holds
fi . c = H1(c) ; ::_thesis: epsilon_ b = lim fi
A4: for b, c being ordinal number holds
( c = H1(b) iff ex fi being Ordinal-Sequence st
( c = last fi & dom fi = succ b & fi . {} = omega |^|^ omega & ( for c being ordinal number st succ c in succ b holds
fi . (succ c) = H3(c,fi . c) ) & ( for c being ordinal number st c in succ b & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) ) by Def7;
thus  H1(b) = H2(b,fi) from ORDINAL2:sch_16(A4, A1, A2, A3); ::_thesis: verum
end;

theorem Th44: :: ORDINAL5:44
for a, b being ordinal number st a in b holds
epsilon_ a in epsilon_ b
proof
let a, b be ordinal number ; ::_thesis: ( a in b implies epsilon_ a in epsilon_ b )
defpred S1[ Ordinal] means ( 1 in epsilon_ $1 & ( for a, b being ordinal number st a in b & b c= $1 holds
epsilon_ a in epsilon_ b ) );
 omega in epsilon_ 0 by Th26, Th41;
then A1: S1[ 0 ] by ORDINAL1:10;
A2: for c being ordinal number st S1[c] holds
S1[ succ c]
proof
let c be ordinal number ; ::_thesis: ( S1[c] implies S1[ succ c] )
assume A3: S1[c] ; ::_thesis: S1[ succ c]
B4: epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th42;
then A4: epsilon_ c in epsilon_ (succ c) by A3, Th26;
hence  1 in epsilon_ (succ c) by A3, ORDINAL1:10; ::_thesis: for a, b being ordinal number st a in b & b c= succ c holds
epsilon_ a in epsilon_ b
let a, b be ordinal number ; ::_thesis: ( a in b & b c= succ c implies epsilon_ a in epsilon_ b )
assume A5: ( a in b & b c= succ c ) ; ::_thesis: epsilon_ a in epsilon_ b
then  a c= c by ORDINAL1:22;
then A6: ( ( b = succ c & ( a = c or a c< c ) ) or b c< succ c ) by A5, XBOOLE_0:def_8;
percases ( b in succ c or ( b = succ c & a in c ) or ( b = succ c & a = c ) ) by A6, ORDINAL1:11;
suppose b in succ c ; ::_thesis: epsilon_ a in epsilon_ b
then  b c= c by ORDINAL1:22;
hence  epsilon_ a in epsilon_ b by A3, A5; ::_thesis: verum
end;
supposeA7: ( b = succ c & a in c ) ; ::_thesis: epsilon_ a in epsilon_ b
then  epsilon_ a in epsilon_ c by A3;
hence  epsilon_ a in epsilon_ b by A4, A7, ORDINAL1:10; ::_thesis: verum
end;
suppose ( b = succ c & a = c ) ; ::_thesis: epsilon_ a in epsilon_ b
hence  epsilon_ a in epsilon_ b by A3, B4, Th26; ::_thesis: verum
end;
end;
end;
A8: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) holds
S1[c]
proof
let c be ordinal number ; ::_thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) implies S1[c] )
assume that
A9: ( c <> {} & c is limit_ordinal ) and
A10: for b being ordinal number st b in c holds
S1[b] ; ::_thesis: S1[c]
deffunc H1( Ordinal) ->  Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
A11: ( dom f = c & ( for b being ordinal number st b in c holds
f . b = H1(b) ) ) from ORDINAL2:sch_3();
 f is increasing
proof
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom f or f . a in f . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom f or f . a in f . b )
assume A12: ( a in b & b in dom f ) ; ::_thesis: f . a in f . b
then  a in c by A11, ORDINAL1:10;
then  ( f . a = H1(a) & f . b = H1(b) & S1[b] ) by A10, A11, A12;
hence  f . a in f . b by A12; ::_thesis: verum
end;
then  Union f is_limes_of f by A9, A11, Th6;
then A13: Union f = lim f by ORDINAL2:def_10
.= epsilon_ c by A9, A11, Th43 ;
A14: 0 in c by A9, ORDINAL3:8;
then  ( 1 in epsilon_ 0 & f . 0 = H1( 0 ) ) by A10, A11;
hence  1 in epsilon_ c by A11, A13, A14, CARD_5:2; ::_thesis: for a, b being ordinal number st a in b & b c= c holds
epsilon_ a in epsilon_ b
let a, b be ordinal number ; ::_thesis: ( a in b & b c= c implies epsilon_ a in epsilon_ b )
assume A15: ( a in b & b c= c ) ; ::_thesis: epsilon_ a in epsilon_ b
then A16: ( b = c or b c< c ) by XBOOLE_0:def_8;
percases ( b in c or b = c ) by A16, ORDINAL1:11;
suppose b in c ; ::_thesis: epsilon_ a in epsilon_ b
hence  epsilon_ a in epsilon_ b by A10, A15; ::_thesis: verum
end;
supposeA17: b = c ; ::_thesis: epsilon_ a in epsilon_ b
 ( succ a in c & a in succ a ) by A9, A15, ORDINAL1:6, ORDINAL1:28;
then A18: ( H1(a) in H1( succ a) & H1( succ a) = f . (succ a) & f . (succ a) in rng f ) by A10, A11, FUNCT_1:def_3;
then  f . (succ a) c= Union f by ZFMISC_1:74;
hence  epsilon_ a in epsilon_ b by A13, A17, A18; ::_thesis: verum
end;
end;
end;
 for c being ordinal number holds S1[c] from ORDINAL2:sch_1(A1, A2, A8);
hence  ( a in b implies epsilon_ a in epsilon_ b ) ; ::_thesis: verum
end;

theorem Th45: :: ORDINAL5:45
for phi being Ordinal-Sequence st ( for c being ordinal number st c in dom phi holds
phi . c = epsilon_ c ) holds
phi is increasing
proof
let f be Ordinal-Sequence; ::_thesis: ( ( for c being ordinal number st c in dom f holds
f . c = epsilon_ c ) implies f is increasing )
assume A1: for c being ordinal number st c in dom f holds
f . c = epsilon_ c ; ::_thesis: f is increasing
let a be ordinal number ; :: according to ORDINAL2:def_12 ::_thesis: for b1 being set holds
( not a in b1 or not b1 in dom f or f . a in f . b1 )
let b be ordinal number ; ::_thesis: ( not a in b or not b in dom f or f . a in f . b )
assume A2: ( a in b & b in dom f ) ; ::_thesis: f . a in f . b
then  ( f . a = epsilon_ a & f . b = epsilon_ b ) by A1, ORDINAL1:10;
hence  f . a in f . b by A2, Th44; ::_thesis: verum
end;

theorem Th46: :: ORDINAL5:46
for b being ordinal number st b <> {} & b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal implies for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi )
assume A1: ( b <> {} & b is limit_ordinal ) ; ::_thesis: for phi being Ordinal-Sequence st dom phi = b & ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi
let f be Ordinal-Sequence; ::_thesis: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = epsilon_ c ) implies epsilon_ b = Union f )
assume A2: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = epsilon_ c ) ) ; ::_thesis: epsilon_ b = Union f
then  f is increasing Ordinal-Sequence by Th45;
then  Union f is_limes_of f by A1, A2, Th6;
then  Union f = lim f by ORDINAL2:def_10;
hence  epsilon_ b = Union f by A1, A2, Th43; ::_thesis: verum
end;

theorem Th47: :: ORDINAL5:47
for b being ordinal number
for x being set st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
proof
let b be ordinal number ; ::_thesis: for x being set st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
let x be set ; ::_thesis: ( not b is empty & b is limit_ordinal implies ( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) ) )
assume A1: ( not b is empty & b is limit_ordinal ) ; ::_thesis: ( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
deffunc H1( Ordinal) ->  Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
A2: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch_3();
A3: Union f = epsilon_ b by A1, A2, Th46;
hereby  ::_thesis: ( ex c being ordinal number st
( c in b & x in epsilon_ c ) implies x in epsilon_ b )
assume  x in epsilon_ b ; ::_thesis: ex c being Ordinal st
( c in b & x in epsilon_ c )
then consider c being set  such that
A4: ( c in dom f & x in f . c ) by A3, CARD_5:2;
reconsider c = c as Ordinal by A4;
take c = c; ::_thesis: ( c in b & x in epsilon_ c )
thus  c in b by A2, A4; ::_thesis: x in epsilon_ c
thus  x in epsilon_ c by A2, A4; ::_thesis: verum
end;
given c being ordinal number  such that A5: ( c in b & x in epsilon_ c ) ; ::_thesis: x in epsilon_ b
 f . c = H1(c) by A2, A5;
hence  x in epsilon_ b by A2, A3, A5, CARD_5:2; ::_thesis: verum
end;

theorem Th48: :: ORDINAL5:48
for a being ordinal number holds a c= epsilon_ a
proof
let a be ordinal number ; ::_thesis: a c= epsilon_ a
defpred S1[ Ordinal] means $1 c= epsilon_ $1;
A1: S1[ 0 ] ;
A2: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume A3: S1[b] ; ::_thesis: S1[ succ b]
 epsilon_ b in epsilon_ (succ b) by Th44, ORDINAL1:6;
then  b in epsilon_ (succ b) by A3, ORDINAL1:12;
hence  S1[ succ b] by ORDINAL1:21; ::_thesis: verum
end;
A4: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) holds
S1[c]
proof
let c be ordinal number ; ::_thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S1[b] ) implies S1[c] )
assume that
 ( c <> {} & c is limit_ordinal ) and
A5: for b being ordinal number st b in c holds
S1[b] ; ::_thesis: S1[c]
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in c or x in epsilon_ c )
assume A6: x in c ; ::_thesis: x in epsilon_ c
then reconsider a = x as Ordinal ;
 ( S1[a] & epsilon_ a in epsilon_ c ) by A5, A6, Th44;
hence  x in epsilon_ c by ORDINAL1:12; ::_thesis: verum
end;
 for b being ordinal number holds S1[b] from ORDINAL2:sch_1(A1, A2, A4);
hence  a c= epsilon_ a ; ::_thesis: verum
end;

theorem Th49: :: ORDINAL5:49
for X being non empty set st ( for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) holds
union X is epsilon Ordinal
proof
let X be non empty set ; ::_thesis: ( ( for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) implies union X is epsilon Ordinal )
assume A1: for x being set st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ; ::_thesis: union X is epsilon Ordinal
then  for x being set st x in X holds
x is Ordinal ;
then reconsider a = union X as Ordinal by ORDINAL1:23;
now__::_thesis:_for_b_being_ordinal_number_st_b_in_a_holds_
succ_b_in_a
let b be ordinal number ; ::_thesis: ( b in a implies succ b in a )
assume  b in a ; ::_thesis: succ b in a
then consider x being set  such that
A2: ( b in x & x in X ) by TARSKI:def_4;
reconsider x = x as epsilon Ordinal by A2, A1;
 succ b in x by A2, ORDINAL1:28;
hence  succ b in a by A2, TARSKI:def_4; ::_thesis: verum
end;
then A3: a is limit_ordinal by ORDINAL1:28;
set z = the Element of X;
 ex e being epsilon Ordinal st
( the Element of X in e & e in X ) by A1;
then A4: a <> {} by TARSKI:def_4;
 a is epsilon
proof
thus  exp (omega,a) c= a :: according to XBOOLE_0:def_10,ORDINAL5:def_5 ::_thesis: a c= exp (omega,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in exp (omega,a) or x in a )
assume  x in exp (omega,a) ; ::_thesis: x in a
then consider b being ordinal number  such that
A5: ( b in a & x in exp (omega,b) ) by A3, A4, Th11;
consider y being set  such that
A6: ( b in y & y in X ) by A5, TARSKI:def_4;
reconsider y = y as epsilon Ordinal by A1, A6;
 exp (omega,b) in exp (omega,y) by A6, ORDINAL4:24;
then  exp (omega,b) in y by Def5;
then  x in y by A5, ORDINAL1:10;
hence  x in a by A6, TARSKI:def_4; ::_thesis: verum
end;
thus  a c= exp (omega,a) by ORDINAL4:32; ::_thesis: verum
end;
hence  union X is epsilon Ordinal ; ::_thesis: verum
end;

theorem Th50: :: ORDINAL5:50
for X being non empty set st ( for x being set st x in X holds
x is epsilon Ordinal ) & ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal
proof
let X be non empty set ; ::_thesis: ( ( for x being set st x in X holds
x is epsilon Ordinal ) & ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) implies union X is epsilon Ordinal )
assume that
A1: for x being set st x in X holds
x is epsilon Ordinal and
A2: for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ; ::_thesis: union X is epsilon Ordinal
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
(_x_is_epsilon_Ordinal_&_ex_e_being_epsilon_Ordinal_st_
(_x_in_e_&_e_in_X_)_)
let x be set ; ::_thesis: ( x in X implies ( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) )
assume A3: x in X ; ::_thesis: ( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) )
hence  x is epsilon Ordinal by A1; ::_thesis: ex e being epsilon Ordinal st
( x in e & e in X )
reconsider a = x as Ordinal by A1, A3;
take e = first_epsilon_greater_than a; ::_thesis: ( x in e & e in X )
thus  ( x in e & e in X ) by A2, A3, Def6; ::_thesis: verum
end;
hence  union X is epsilon Ordinal by Th49; ::_thesis: verum
end;

registration
let a be ordinal number ;
cluster epsilon_ a ->  epsilon ;
coherence
 epsilon_ a is epsilon
proof
deffunc H1( Ordinal) ->  Ordinal = epsilon_ a;
defpred S1[ Ordinal] means H1(a) is epsilon ;
A1: S1[ {} ] by Th36, Th41;
A2: for b being ordinal number st S1[b] holds
S1[ succ b]
proof
let b be ordinal number ; ::_thesis: ( S1[b] implies S1[ succ b] )
assume  S1[b] ; ::_thesis: S1[ succ b]
then  first_epsilon_greater_than (epsilon_ b) = (epsilon_ b) |^|^ omega by Th40
.= epsilon_ (succ b) by Th42 ;
hence  S1[ succ b] ; ::_thesis: verum
end;
A3: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) holds
S1[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S1[c] ) implies S1[b] )
assume that
A4: ( b <> {} & b is limit_ordinal ) and
A5: for c being ordinal number st c in b holds
S1[c] ; ::_thesis: S1[b]
consider f being Ordinal-Sequence such that
A6: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch_3();
A7: H1(b) = Union f by A4, A6, Th46;
set X = rng f;
 0 in b by A4, ORDINAL3:8;
then  f . 0 in rng f by A6, FUNCT_1:def_3;
then reconsider X = rng f as non empty set ;
A8: now__::_thesis:_for_x_being_set_st_x_in_X_holds_
x_is_epsilon_Ordinal
let x be set ; ::_thesis: ( x in X implies x is epsilon Ordinal )
assume  x in X ; ::_thesis: x is epsilon Ordinal
then consider a being set  such that
A9: ( a in dom f & f . a = x ) by FUNCT_1:def_3;
reconsider a = a as Ordinal by A9;
 x = H1(a) by A6, A9;
hence  x is epsilon Ordinal by A5, A6, A9; ::_thesis: verum
end;
now__::_thesis:_for_x_being_Ordinal_st_x_in_X_holds_
first_epsilon_greater_than_x_in_X
let x be Ordinal; ::_thesis: ( x in X implies first_epsilon_greater_than x in X )
assume A10: x in X ; ::_thesis: first_epsilon_greater_than x in X
then consider a being set  such that
A11: ( a in dom f & f . a = x ) by FUNCT_1:def_3;
reconsider a = a as Ordinal by A11;
A12: succ a in b by A4, A6, A11, ORDINAL1:28;
reconsider e = x as epsilon Ordinal by A8, A10;
 e = H1(a) by A6, A11;
then  first_epsilon_greater_than e = H1(a) |^|^ omega by Th40
.= H1( succ a) by Th42
.= f . (succ a) by A6, A12 ;
hence  first_epsilon_greater_than x in X by A6, A12, FUNCT_1:def_3; ::_thesis: verum
end;
hence  S1[b] by A7, A8, Th50; ::_thesis: verum
end;
 for a being ordinal number holds S1[a] from ORDINAL2:sch_1(A1, A2, A3);
hence  epsilon_ a is epsilon ; ::_thesis: verum
end;
end;

theorem :: ORDINAL5:51
for a being ordinal number st a is epsilon holds
ex b being ordinal number st a = epsilon_ b
proof
let a be ordinal number ; ::_thesis: ( a is epsilon implies ex b being ordinal number st a = epsilon_ b )
defpred S1[ set ] means  ex b being ordinal number st $1 = epsilon_ b;
defpred S2[ Ordinal] means  for e being epsilon Ordinal st e in epsilon_ $1 holds
S1[e];
A1: S2[ {} ]
proof
let e be epsilon Ordinal; ::_thesis: ( e in epsilon_ {} implies S1[e] )
 0 in e by ORDINAL3:8;
then  first_epsilon_greater_than 0 c= e by Def6;
then  ( e in epsilon_ 0 implies e in e ) by Th36, Th41;
hence  ( e in epsilon_ {} implies S1[e] ) ; ::_thesis: verum
end;
A2: for c being ordinal number st S2[c] holds
S2[ succ c]
proof
let c be ordinal number ; ::_thesis: ( S2[c] implies S2[ succ c] )
assume A3: S2[c] ; ::_thesis: S2[ succ c]
let e be epsilon Ordinal; ::_thesis: ( e in epsilon_ (succ c) implies S1[e] )
assume A4: e in epsilon_ (succ c) ; ::_thesis: S1[e]
A5: epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th42
.= first_epsilon_greater_than (epsilon_ c) by Th40 ;
percases ( e in epsilon_ c or e = epsilon_ c or epsilon_ c in e ) by ORDINAL1:14;
suppose e in epsilon_ c ; ::_thesis: S1[e]
hence  S1[e] by A3; ::_thesis: verum
end;
suppose e = epsilon_ c ; ::_thesis: S1[e]
hence  S1[e] ; ::_thesis: verum
end;
suppose epsilon_ c in e ; ::_thesis: S1[e]
then  epsilon_ (succ c) c= e by A5, Def6;
then  e in e by A4;
hence  S1[e] ; ::_thesis: verum
end;
end;
end;
A6: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S2[c] ) holds
S2[b]
proof
let b be ordinal number ; ::_thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S2[c] ) implies S2[b] )
assume that
A7: ( b <> {} & b is limit_ordinal ) and
A8: for c being ordinal number st c in b holds
S2[c] ; ::_thesis: S2[b]
let e be epsilon Ordinal; ::_thesis: ( e in epsilon_ b implies S1[e] )
assume  e in epsilon_ b ; ::_thesis: S1[e]
then  ex c being ordinal number st
( c in b & e in epsilon_ c ) by A7, Th47;
hence  S1[e] by A8; ::_thesis: verum
end;
A9: for b being ordinal number holds S2[b] from ORDINAL2:sch_1(A1, A2, A6);
 ( a c= epsilon_ a & epsilon_ a in epsilon_ (succ a) ) by Th44, Th48, ORDINAL1:6;
hence  ( a is epsilon implies ex b being ordinal number st a = epsilon_ b ) by A9, ORDINAL1:12; ::_thesis: verum
end;

begin

definition
let A be finite Ordinal-Sequence;
func Sum^ A ->  Ordinal means :Def8: :: ORDINAL5:def 8
 ex f being Ordinal-Sequence st
( it = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) );
correctness
existence
ex b1 being Ordinal ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) );
uniqueness
for b1, b2 being Ordinal st ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) holds
b1 = b2;
proof
deffunc H1( Ordinal, Ordinal) ->  set = $2 +^ (A . $1);
deffunc H2( Ordinal, Ordinal-Sequence) ->  set = Union $2;
set b = dom A;
A1: ( ex F being Ordinal ex fi being Ordinal-Sequence st
( F = last fi & dom fi = succ (dom A) & fi . {} = 0 & ( for c being Ordinal st succ c in succ (dom A) holds
fi . (succ c) = H1(c,fi . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> {} & c is limit_ordinal holds
fi . c = H2(c,fi | c) ) ) & ( for A1, A2 being Ordinal st ex fi being Ordinal-Sequence st
( A1 = last fi & dom fi = succ (dom A) & fi . {} = 0 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) & ex fi being Ordinal-Sequence st
( A2 = last fi & dom fi = succ (dom A) & fi . {} = 0 & ( for C being Ordinal st succ C in succ (dom A) holds
fi . (succ C) = H1(C,fi . C) ) & ( for C being Ordinal st C in succ (dom A) & C <> {} & C is limit_ordinal holds
fi . C = H2(C,fi | C) ) ) holds
A1 = A2 ) ) from ORDINAL2:sch_13();
then consider a being ordinal number , f being Ordinal-Sequence such that
A2: ( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for c being Ordinal st succ c in succ (dom A) holds
f . (succ c) = H1(c,f . c) ) & ( for c being Ordinal st c in succ (dom A) & c <> {} & c is limit_ordinal holds
f . c = H2(c,f | c) ) ) ;
hereby  ::_thesis: for b1, b2 being Ordinal st ex f being Ordinal-Sequence st
( b1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) holds
b1 = b2
take a = a; ::_thesis: ex f being Ordinal-Sequence st
( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) )
take f = f; ::_thesis: ( a = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) )
thus  ( a = last f & dom f = succ (dom A) & f . 0 = 0 ) by A2; ::_thesis: for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n)
let n be Nat; ::_thesis: ( n in dom A implies f . (n + 1) = (f . n) +^ (A . n) )
assume  n in dom A ; ::_thesis: f . (n + 1) = (f . n) +^ (A . n)
then  succ n c= dom A by ORDINAL1:21;
then  ( succ n in succ (dom A) & n + 1 = succ n ) by NAT_1:38, ORDINAL1:22;
hence  f . (n + 1) = (f . n) +^ (A . n) by A2; ::_thesis: verum
end;
let a1, a2 be Ordinal; ::_thesis: ( ex f being Ordinal-Sequence st
( a1 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) & ex f being Ordinal-Sequence st
( a2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) implies a1 = a2 )
given f1 being Ordinal-Sequence such that A3: ( a1 = last f1 & dom f1 = succ (dom A) & f1 . 0 = 0 & ( for n being Nat st n in dom A holds
f1 . (n + 1) = (f1 . n) +^ (A . n) ) ) ; ::_thesis: ( for f being Ordinal-Sequence holds
( not a2 = last f or not dom f = succ (dom A) or not f . 0 = 0 or ex n being Nat st
( n in dom A & not f . (n + 1) = (f . n) +^ (A . n) ) ) or a1 = a2 )
given f2 being Ordinal-Sequence such that A4: ( a2 = last f2 & dom f2 = succ (dom A) & f2 . 0 = 0 & ( for n being Nat st n in dom A holds
f2 . (n + 1) = (f2 . n) +^ (A . n) ) ) ; ::_thesis: a1 = a2
reconsider b = dom A as finite Ordinal ;
A5: ( succ b in omega & b in omega ) by CARD_1:61;
A6: for c being Ordinal st succ c in succ b holds
f1 . (succ c) = H1(c,f1 . c)
proof
let c be ordinal number ; ::_thesis: ( succ c in succ b implies f1 . (succ c) = H1(c,f1 . c) )
assume  succ c in succ b ; ::_thesis: f1 . (succ c) = H1(c,f1 . c)
then A7: c in b by ORDINAL3:3;
then reconsider n = c as Element of omega ;
 f1 . (n + 1) = H1(n,f1 . n) by A3, A7;
hence  f1 . (succ c) = H1(c,f1 . c) by NAT_1:38; ::_thesis: verum
end;
A8: for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f1 . c = H2(c,f1 | c)
proof
let c be Ordinal; ::_thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f1 . c = H2(c,f1 | c) )
assume A9: ( c in succ b & c <> {} & c is limit_ordinal ) ; ::_thesis: f1 . c = H2(c,f1 | c)
then  0 in c by ORDINAL3:8;
then  ( c in omega & omega c= c ) by A9, A5, ORDINAL1:10, ORDINAL1:def_11;
hence  f1 . c = H2(c,f1 | c) ; ::_thesis: verum
end;
A10: for c being Ordinal st succ c in succ b holds
f2 . (succ c) = H1(c,f2 . c)
proof
let c be ordinal number ; ::_thesis: ( succ c in succ b implies f2 . (succ c) = H1(c,f2 . c) )
assume  succ c in succ b ; ::_thesis: f2 . (succ c) = H1(c,f2 . c)
then A11: c in b by ORDINAL3:3;
then reconsider n = c as Element of omega ;
 f2 . (n + 1) = H1(n,f2 . n) by A4, A11;
hence  f2 . (succ c) = H1(c,f2 . c) by NAT_1:38; ::_thesis: verum
end;
 for c being Ordinal st c in succ b & c <> {} & c is limit_ordinal holds
f2 . c = H2(c,f2 | c)
proof
let c be Ordinal; ::_thesis: ( c in succ b & c <> {} & c is limit_ordinal implies f2 . c = H2(c,f2 | c) )
assume A12: ( c in succ b & c <> {} & c is limit_ordinal ) ; ::_thesis: f2 . c = H2(c,f2 | c)
then  0 in c by ORDINAL3:8;
then  ( c in omega & omega c= c ) by A12, A5, ORDINAL1:10, ORDINAL1:def_11;
hence  f2 . c = H2(c,f2 | c) ; ::_thesis: verum
end;
hence  a1 = a2 by A1, A3, A4, A6, A8, A10; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Sum^ ORDINAL5:def_8_:_
 for A being finite Ordinal-Sequence
for b2 being Ordinal holds
( b2 = Sum^ A iff ex f being Ordinal-Sequence st
( b2 = last f & dom f = succ (dom A) & f . 0 = 0 & ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) );

theorem Th52: :: ORDINAL5:52
Sum^ {} = 0
proof
reconsider A = {} as finite Ordinal-Sequence ;
consider f being Ordinal-Sequence such that
A1: Sum^ A = last f and
A2: dom f = succ (dom A) and
A3: f . 0 = 0 and
 for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) by Def8;
 ( dom f = succ 0 implies last f = f . 0 ) by ORDINAL2:6;
hence  Sum^ {} = 0 by A1, A2, A3; ::_thesis: verum
end;

theorem Th53: :: ORDINAL5:53
for a being ordinal number holds Sum^ <%a%> = a
proof
let a be ordinal number ; ::_thesis: Sum^ <%a%> = a
consider f being Ordinal-Sequence such that
A1: ( Sum^ <%a%> = last f & dom f = succ (dom <%a%>) & f . 0 = 0 & ( for n being Nat st n in dom <%a%> holds
f . (n + 1) = (f . n) +^ (<%a%> . n) ) ) by Def8;
A2: ( dom <%a%> = 1 & <%a%> . 0 = a ) by AFINSQ_1:def_4;
 0 in 1 by NAT_1:44;
then f . (0 + 1) = 0 +^ a by A1, A2
.= a by ORDINAL2:30 ;
hence  Sum^ <%a%> = a by A1, A2, ORDINAL2:6; ::_thesis: verum
end;

theorem Th54: :: ORDINAL5:54
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
proof
let a be ordinal number ; ::_thesis: for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
let A be finite Ordinal-Sequence; ::_thesis: Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
consider f being Ordinal-Sequence such that
A1: ( Sum^ (A ^ <%a%>) = last f & dom f = succ (dom (A ^ <%a%>)) & f . 0 = 0 & ( for n being Nat st n in dom (A ^ <%a%>) holds
f . (n + 1) = (f . n) +^ ((A ^ <%a%>) . n) ) ) by Def8;
consider g being Ordinal-Sequence such that
A2: ( Sum^ A = last g & dom g = succ (dom A) & g . 0 = 0 & ( for n being Nat st n in dom A holds
g . (n + 1) = (g . n) +^ (A . n) ) ) by Def8;
 dom <%a%> = 1 by AFINSQ_1:def_4;
then A3: ( dom (A ^ <%a%>) = (dom A) +^ 1 & (dom A) +^ 1 = succ (dom A) ) by ORDINAL2:31, ORDINAL4:def_1;
reconsider dA = dom A as Element of NAT by ORDINAL1:def_12;
A4: dom A in succ (dom A) by ORDINAL1:6;
defpred S1[ Nat] means ( $1 in succ (dom A) implies f . $1 = g . $1 );
A5: S1[ 0 ] by A1, A2;
A6: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume that
A7: S1[n] and
A8: n + 1 in succ (dom A) ; ::_thesis: f . (n + 1) = g . (n + 1)
 n + 1 = succ n by NAT_1:38;
then A9: n in dom A by A8, ORDINAL3:3;
then  n in succ (dom A) by A4, ORDINAL1:10;
then  ( g . (n + 1) = (g . n) +^ (A . n) & f . (n + 1) = (f . n) +^ ((A ^ <%a%>) . n) ) by A1, A2, A3, A9;
hence  f . (n + 1) = g . (n + 1) by A7, A9, A4, ORDINAL1:10, ORDINAL4:def_1; ::_thesis: verum
end;
A11: for n being Nat holds S1[n] from NAT_1:sch_2(A5, A6);
thus  Sum^ (A ^ <%a%>) = f . ((dom A) +^ 1) by A1, A3, ORDINAL2:6
.= f . (dA + 1) by CARD_2:36
.= (f . (dom A)) +^ ((A ^ <%a%>) . (len A)) by A1, A3, ORDINAL1:6
.= (f . (dom A)) +^ a by AFINSQ_1:36
.= (g . (dom A)) +^ a by ORDINAL1:6, A11
.= (Sum^ A) +^ a by A2, ORDINAL2:6 ; ::_thesis: verum
end;

theorem Th55: :: ORDINAL5:55
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
proof
let a be ordinal number ; ::_thesis: for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
defpred S1[ finite T-Sequence] means  for f being finite Ordinal-Sequence st f = $1 holds
Sum^ (<%a%> ^ f) = a +^ (Sum^ f);
 Sum^ (<%a%> ^ {}) = a by Th53;
then A1: S1[ {} ] by Th52, ORDINAL2:27;
A2: for f being finite T-Sequence
for x being set st S1[f] holds
S1[f ^ <%x%>]
proof
let f be finite T-Sequence; ::_thesis: for x being set st S1[f] holds
S1[f ^ <%x%>]
let x be set ; ::_thesis: ( S1[f] implies S1[f ^ <%x%>] )
assume A3: S1[f] ; ::_thesis: S1[f ^ <%x%>]
let g be finite Ordinal-Sequence; ::_thesis: ( g = f ^ <%x%> implies Sum^ (<%a%> ^ g) = a +^ (Sum^ g) )
consider b being ordinal number  such that
A4: rng g c= b by ORDINAL2:def_4;
assume A5: g = f ^ <%x%> ; ::_thesis: Sum^ (<%a%> ^ g) = a +^ (Sum^ g)
then  rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:26;
then A6: ( rng f c= b & rng <%x%> c= b ) by A4, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def_4;
 rng <%x%> = {x} by AFINSQ_1:33;
then  x in b by A6, ZFMISC_1:31;
then reconsider x = x as Ordinal ;
thus  Sum^ (<%a%> ^ g) = Sum^ ((<%a%> ^ f9) ^ <%x%>) by A5, AFINSQ_1:27
.= (Sum^ (<%a%> ^ f9)) +^ x by Th54
.= (a +^ (Sum^ f9)) +^ x by A3
.= a +^ ((Sum^ f9) +^ x) by ORDINAL3:30
.= a +^ (Sum^ g) by A5, Th54 ; ::_thesis: verum
end;
 for f being finite T-Sequence holds S1[f] from AFINSQ_1:sch_3(A1, A2);
hence  for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A) ; ::_thesis: verum
end;

theorem Th56: :: ORDINAL5:56
for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A
proof
let A be finite Ordinal-Sequence; ::_thesis: A . 0 c= Sum^ A
defpred S1[ finite T-Sequence] means  for A being finite Ordinal-Sequence st $1 = A holds
A . 0 c= Sum^ A;
A1: S1[ {} ] ;
A2: for f being finite T-Sequence
for x being set st S1[f] holds
S1[f ^ <%x%>]
proof
let f be finite T-Sequence; ::_thesis: for x being set st S1[f] holds
S1[f ^ <%x%>]
let x be set ; ::_thesis: ( S1[f] implies S1[f ^ <%x%>] )
assume A3: S1[f] ; ::_thesis: S1[f ^ <%x%>]
let g be finite Ordinal-Sequence; ::_thesis: ( f ^ <%x%> = g implies g . 0 c= Sum^ g )
consider b being ordinal number  such that
A4: rng g c= b by ORDINAL2:def_4;
assume A5: g = f ^ <%x%> ; ::_thesis: g . 0 c= Sum^ g
then  rng g = (rng f) \/ (rng <%x%>) by AFINSQ_1:26;
then A6: ( rng f c= b & rng <%x%> c= b ) by A4, XBOOLE_1:11;
then reconsider f9 = f as finite Ordinal-Sequence by ORDINAL2:def_4;
 rng <%x%> = {x} by AFINSQ_1:33;
then  x in b by A6, ZFMISC_1:31;
then reconsider x = x as Ordinal ;
percases ( f = {} or f <> {} ) ;
suppose f = {} ; ::_thesis: g . 0 c= Sum^ g
then  g = {} ^ <%x%> by A5;
then  g = <%x%> ;
then  ( g . 0 = x & Sum^ g = x ) by Th53, AFINSQ_1:def_4;
hence  g . 0 c= Sum^ g ; ::_thesis: verum
end;
suppose f <> {} ; ::_thesis: g . 0 c= Sum^ g
then  ( 0 in dom f9 & Sum^ g = (Sum^ f9) +^ x ) by A5, Th54, ORDINAL3:8;
then  ( g . 0 = f9 . 0 & f9 . 0 c= Sum^ f9 & Sum^ f9 c= Sum^ g ) by A3, A5, ORDINAL3:24, ORDINAL4:def_1;
hence  g . 0 c= Sum^ g by XBOOLE_1:1; ::_thesis: verum
end;
end;
end;
 for f being finite T-Sequence holds S1[f] from AFINSQ_1:sch_3(A1, A2);
hence  A . 0 c= Sum^ A ; ::_thesis: verum
end;

definition
let a be ordinal number ;
attra is Cantor-component  means :Def9: :: ORDINAL5:def 9
 ex b being ordinal number ex n being Nat st
( 0 in n & a = n *^ (exp (omega,b)) );
end;

:: deftheorem Def9 defines Cantor-component ORDINAL5:def_9_:_
 for a being ordinal number holds
( a is Cantor-component iff ex b being ordinal number ex n being Nat st
( 0 in n & a = n *^ (exp (omega,b)) ) );

registration
cluster ordinal Cantor-component  ->  non empty for set ;
coherence
 for b1 being Ordinal st b1 is Cantor-component holds
not b1 is empty
proof
let a be ordinal number ; ::_thesis: ( a is Cantor-component implies not a is empty )
given b being ordinal number , n being Nat such that A1: ( 0 in n & a = n *^ (exp (omega,b)) ) ; :: according to ORDINAL5:def_9 ::_thesis: not a is empty
 exp (omega,b) <> 0 by ORDINAL4:22;
hence  not a is empty by A1, ORDINAL3:31; ::_thesis: verum
end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal Cantor-component for set ;
existence
 ex b1 being Ordinal st b1 is Cantor-component
proof
take  1 *^ (exp (omega,1)) ; ::_thesis: 1 *^ (exp (omega,1)) is Cantor-component
take  1 ; :: according to ORDINAL5:def_9 ::_thesis: ex n being Nat st
( 0 in n & 1 *^ (exp (omega,1)) = n *^ (exp (omega,1)) )
take  1 ; ::_thesis: ( 0 in 1 & 1 *^ (exp (omega,1)) = 1 *^ (exp (omega,1)) )
thus  ( 0 in 1 & 1 *^ (exp (omega,1)) = 1 *^ (exp (omega,1)) ) by NAT_1:44; ::_thesis: verum
end;
end;

definition
let a, b be ordinal number ;
funcb -exponent a ->  Ordinal means :Def10: :: ORDINAL5:def 10
( exp (b,it) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= it ) ) if ( 1 in b & 0 in a )
otherwise it = 0 ;
existence
 ( ( 1 in b & 0 in a implies ex b1 being Ordinal st
( exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) ) ) & ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 ) )
proof
hereby  ::_thesis: ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 )
assume A1: ( 1 in b & 0 in a ) ; ::_thesis: ex c being ordinal number st
( exp (b,c) c= a & ( for d being ordinal number st exp (b,d) c= a holds
not d c/= c ) )
defpred S1[ Ordinal] means a c= exp (b,$1);
 a c= exp (b,a) by A1, ORDINAL4:32;
then A2: ex c being ordinal number st S1[c] ;
consider c being ordinal number  such that
A3: ( S1[c] & ( for d being ordinal number st S1[d] holds
c c= d ) ) from ORDINAL1:sch_1(A2);
 0 in 1 by NAT_1:44;
then A4: 0 in b by A1, ORDINAL1:10;
percases ( a = exp (b,c) or a c< exp (b,c) ) by A3, XBOOLE_0:def_8;
supposeA5: a = exp (b,c) ; ::_thesis: ex c being ordinal number st
( exp (b,c) c= a & ( for d being ordinal number st exp (b,d) c= a holds
not d c/= c ) )
take c = c; ::_thesis: ( exp (b,c) c= a & ( for d being ordinal number st exp (b,d) c= a holds
not d c/= c ) )
thus  exp (b,c) c= a by A5; ::_thesis: for d being ordinal number st exp (b,d) c= a holds
not d c/= c
let d be ordinal number ; ::_thesis: ( exp (b,d) c= a implies not d c/= c )
assume A6: ( exp (b,d) c= a & d c/= c ) ; ::_thesis: contradiction
then  c in d by ORDINAL1:16;
then  a in exp (b,d) by A1, A5, ORDINAL4:24;
then  a in a by A6;
hence  contradiction ; ::_thesis: verum
end;
supposeB7: a c< exp (b,c) ; ::_thesis: ex d being ordinal number st
( exp (b,d) c= a & ( for e being ordinal number st exp (b,e) c= a holds
not e c/= d ) )
then A7: a in exp (b,c) by ORDINAL1:11;
 succ 0 c= a by A1, ORDINAL1:21;
then  ( 1 in exp (b,c) & exp (b,0) = 1 ) by B7, ORDINAL1:11, ORDINAL1:12, ORDINAL2:43;
then A8: c <> 0 ;
now__::_thesis:_not_c_is_limit_ordinal
assume  c is limit_ordinal ; ::_thesis: contradiction
then consider d being ordinal number  such that
A9: ( d in c & a in exp (b,d) ) by A8, A4, A7, Th11;
 S1[d] by A9, ORDINAL1:def_2;
then  c c= d by A3;
then  d in d by A9;
hence  contradiction ; ::_thesis: verum
end;
then consider d being ordinal number  such that
A10: c = succ d by ORDINAL1:29;
take d = d; ::_thesis: ( exp (b,d) c= a & ( for e being ordinal number st exp (b,e) c= a holds
not e c/= d ) )
thus  exp (b,d) c= a ::_thesis: for e being ordinal number st exp (b,e) c= a holds
not e c/= d
proof
assume  exp (b,d) c/= a ; ::_thesis: contradiction
then  a c= exp (b,d) ;
then  c c= d by A3;
then  d in d by A10, ORDINAL1:21;
hence  contradiction ; ::_thesis: verum
end;
let e be ordinal number ; ::_thesis: ( exp (b,e) c= a implies not e c/= d )
assume A11: ( exp (b,e) c= a & e c/= d ) ; ::_thesis: contradiction
then  d in e by ORDINAL1:16;
then  c c= e by A10, ORDINAL1:21;
then  exp (b,c) c= exp (b,e) by A1, ORDINAL4:27;
then  a in exp (b,e) by A7;
then  a in a by A11;
hence  contradiction ; ::_thesis: verum
end;
end;
end;
thus  ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Ordinal holds
( ( 1 in b & 0 in a & exp (b,b1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) & exp (b,b2) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b2 ) implies b1 = b2 ) & ( ( not 1 in b or not 0 in a ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof
let d1, d2 be Ordinal; ::_thesis: ( ( 1 in b & 0 in a & exp (b,d1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= d1 ) & exp (b,d2) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= d2 ) implies d1 = d2 ) & ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 ) )
hereby  ::_thesis: ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 )
assume that
 ( 1 in b & 0 in a ) and
A12: ( exp (b,d1) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= d1 ) ) and
A13: ( exp (b,d2) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= d2 ) ) ; ::_thesis: d1 = d2
thus  d1 = d2 ::_thesis: verum
proof
thus  d1 c= d2 by A12, A13; :: according to XBOOLE_0:def_10 ::_thesis: d2 c= d1
thus  d2 c= d1 by A12, A13; ::_thesis: verum
end;
end;
thus  ( ( not 1 in b or not 0 in a ) & d1 = 0 & d2 = 0 implies d1 = d2 ) ; ::_thesis: verum
end;
consistency
 for b1 being Ordinal holds verum ;
end;

:: deftheorem Def10 defines -exponent ORDINAL5:def_10_:_
 for a, b being ordinal number
for b3 being Ordinal holds
( ( 1 in b & 0 in a implies ( b3 = b -exponent a iff ( exp (b,b3) c= a & ( for c being ordinal number st exp (b,c) c= a holds
c c= b3 ) ) ) ) & ( ( not 1 in b or not 0 in a ) implies ( b3 = b -exponent a iff b3 = 0 ) ) );

Lm2:  0 in 1
by NAT_1:44;

theorem Th57: :: ORDINAL5:57
for b, a being ordinal number st 1 in b holds
a in exp (b,(succ (b -exponent a)))
proof
let b, a be ordinal number ; ::_thesis: ( 1 in b implies a in exp (b,(succ (b -exponent a))) )
assume A1: 1 in b ; ::_thesis: a in exp (b,(succ (b -exponent a)))
percases ( 0 in a or a = 0 ) by ORDINAL3:8;
supposeA2: 0 in a ; ::_thesis: a in exp (b,(succ (b -exponent a)))
assume  not a in exp (b,(succ (b -exponent a))) ; ::_thesis: contradiction
then  exp (b,(succ (b -exponent a))) c= a by ORDINAL1:16;
then  ( succ (b -exponent a) c= b -exponent a & b -exponent a in succ (b -exponent a) ) by A1, A2, Def10, ORDINAL1:6;
then  b -exponent a in b -exponent a ;
hence  contradiction ; ::_thesis: verum
end;
supposeA3: a = 0 ; ::_thesis: a in exp (b,(succ (b -exponent a)))
then  b -exponent a = 0 by Def10;
then  exp (b,(succ (b -exponent a))) = b by ORDINAL2:46;
hence  a in exp (b,(succ (b -exponent a))) by A1, A3, Lm2, ORDINAL1:10; ::_thesis: verum
end;
end;
end;

theorem Th58: :: ORDINAL5:58
for b, a being ordinal number
for n being Nat st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a
proof
let b, a be ordinal number ; ::_thesis: for n being Nat st 0 in n & n in b holds
b -exponent (n *^ (exp (b,a))) = a
let n be Nat; ::_thesis: ( 0 in n & n in b implies b -exponent (n *^ (exp (b,a))) = a )
assume A1: ( 0 in n & n in b ) ; ::_thesis: b -exponent (n *^ (exp (b,a))) = a
then A2: succ 0 c= n by ORDINAL1:21;
then A3: ( 1 *^ (exp (b,a)) = exp (b,a) & 1 *^ (exp (b,a)) c= n *^ (exp (b,a)) ) by ORDINAL2:39, ORDINAL2:41;
 ( exp (b,a) <> 0 & n <> 0 ) by A1, ORDINAL4:22;
then  0 <> n *^ (exp (b,a)) by ORDINAL3:31;
then A5: ( 1 in b & 0 in n *^ (exp (b,a)) ) by A2, A1, ORDINAL1:12, ORDINAL3:8;
now__::_thesis:_for_c_being_ordinal_number_st_exp_(b,c)_c=_n_*^_(exp_(b,a))_holds_
not_c_c/=_a
let c be ordinal number ; ::_thesis: ( exp (b,c) c= n *^ (exp (b,a)) implies not c c/= a )
assume A6: ( exp (b,c) c= n *^ (exp (b,a)) & c c/= a ) ; ::_thesis: contradiction
then  a in c by ORDINAL1:16;
then  succ a c= c by ORDINAL1:21;
then A7: exp (b,(succ a)) c= exp (b,c) by A1, ORDINAL4:27;
 exp (b,(succ a)) = b *^ (exp (b,a)) by ORDINAL2:44;
then  b *^ (exp (b,a)) c= n *^ (exp (b,a)) by A6, A7, XBOOLE_1:1;
then  b c= n by A1, ORDINAL4:22, ORDINAL3:35;
then  n in n by A1;
hence  contradiction ; ::_thesis: verum
end;
hence  b -exponent (n *^ (exp (b,a))) = a by A3, A5, Def10; ::_thesis: verum
end;

theorem Th59: :: ORDINAL5:59
for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
a div^ (exp (b,c)) in b
proof
let a, b, c be ordinal number ; ::_thesis: ( 0 in a & 1 in b & c = b -exponent a implies a div^ (exp (b,c)) in b )
assume A1: ( 0 in a & 1 in b & c = b -exponent a ) ; ::_thesis: a div^ (exp (b,c)) in b
set n = a div^ (exp (b,c));
 exp (b,c) <> 0 by A1, ORDINAL4:22;
then consider d being ordinal number  such that
A2: ( a = ((a div^ (exp (b,c))) *^ (exp (b,c))) +^ d & d in exp (b,c) ) by ORDINAL3:def_6;
assume  not a div^ (exp (b,c)) in b ; ::_thesis: contradiction
then  b *^ (exp (b,c)) c= (a div^ (exp (b,c))) *^ (exp (b,c)) by ORDINAL1:16, ORDINAL2:41;
then  ( exp (b,(succ c)) c= (a div^ (exp (b,c))) *^ (exp (b,c)) & (a div^ (exp (b,c))) *^ (exp (b,c)) c= a ) by A2, ORDINAL2:44, ORDINAL3:24;
then  exp (b,(succ c)) c= a by XBOOLE_1:1;
then  ( succ c c= c & c in succ c ) by A1, Def10, ORDINAL1:6;
then  c in c ;
hence  contradiction ; ::_thesis: verum
end;

theorem Th60: :: ORDINAL5:60
for a, b, c being ordinal number st 0 in a & 1 in b & c = b -exponent a holds
0 in a div^ (exp (b,c))
proof
let a, b, c be ordinal number ; ::_thesis: ( 0 in a & 1 in b & c = b -exponent a implies 0 in a div^ (exp (b,c)) )
assume A1: ( 0 in a & 1 in b & c = b -exponent a ) ; ::_thesis: 0 in a div^ (exp (b,c))
set n = a div^ (exp (b,c));
 exp (b,c) <> 0 by A1, ORDINAL4:22;
then consider d being ordinal number  such that
A2: ( a = ((a div^ (exp (b,c))) *^ (exp (b,c))) +^ d & d in exp (b,c) ) by ORDINAL3:def_6;
assume  not 0 in a div^ (exp (b,c)) ; ::_thesis: contradiction
then  a div^ (exp (b,c)) = 0 by ORDINAL3:8;
then a = 0 +^ d by A2, ORDINAL2:35
.= d by ORDINAL2:30 ;
then  exp (b,c) c= d by A1, Def10;
then  d in d by A2;
hence  contradiction ; ::_thesis: verum
end;

theorem Th61: :: ORDINAL5:61
for b, a, c being ordinal number st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)
proof
let b, a, c be ordinal number ; ::_thesis: ( b <> 0 implies a mod^ (exp (b,c)) in exp (b,c) )
assume A1: b <> 0 ; ::_thesis: a mod^ (exp (b,c)) in exp (b,c)
set n = a div^ (exp (b,c));
 exp (b,c) <> 0 by A1, ORDINAL4:22;
then consider d being ordinal number  such that
A2: ( a = ((a div^ (exp (b,c))) *^ (exp (b,c))) +^ d & d in exp (b,c) ) by ORDINAL3:def_6;
d = a -^ ((a div^ (exp (b,c))) *^ (exp (b,c))) by A2, ORDINAL3:52
.= a mod^ (exp (b,c)) by ORDINAL3:def_7 ;
hence  a mod^ (exp (b,c)) in exp (b,c) by A2; ::_thesis: verum
end;

theorem Th62: :: ORDINAL5:62
for a being ordinal number st 0 in a holds
ex n being Nat ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
proof
let a be ordinal number ; ::_thesis: ( 0 in a implies ex n being Nat ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) ) )
assume A1: 0 in a ; ::_thesis: ex n being Nat ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
set c = omega -exponent a;
set n = a div^ (exp (omega,(omega -exponent a)));
set b = a mod^ (exp (omega,(omega -exponent a)));
 a div^ (exp (omega,(omega -exponent a))) in omega by A1, Th59;
then reconsider n = a div^ (exp (omega,(omega -exponent a))) as Nat ;
take  n ; ::_thesis: ex c being ordinal number st
( a = (n *^ (exp (omega,(omega -exponent a)))) +^ c & 0 in n & c in exp (omega,(omega -exponent a)) )
take  a mod^ (exp (omega,(omega -exponent a))) ; ::_thesis: ( a = (n *^ (exp (omega,(omega -exponent a)))) +^ (a mod^ (exp (omega,(omega -exponent a)))) & 0 in n & a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) )
thus  a = (n *^ (exp (omega,(omega -exponent a)))) +^ (a mod^ (exp (omega,(omega -exponent a)))) by ORDINAL3:65; ::_thesis: ( 0 in n & a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) )
thus  0 in n by A1, Th60; ::_thesis: a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a))
thus  a mod^ (exp (omega,(omega -exponent a))) in exp (omega,(omega -exponent a)) by Th61; ::_thesis: verum
end;

theorem Th63: :: ORDINAL5:63
for c, b, a being ordinal number st 1 in c & c -exponent b in c -exponent a holds
b in a
proof
let c, b, a be ordinal number ; ::_thesis: ( 1 in c & c -exponent b in c -exponent a implies b in a )
assume A1: ( 1 in c & c -exponent b in c -exponent a ) ; ::_thesis: b in a
then  succ (c -exponent b) c= c -exponent a by ORDINAL1:21;
then A2: exp (c,(succ (c -exponent b))) c= exp (c,(c -exponent a)) by A1, ORDINAL4:27;
A3: 0 in a by A1, Def10;
 b in exp (c,(succ (c -exponent b))) by A1, Th57;
then  ( b in exp (c,(c -exponent a)) & exp (c,(c -exponent a)) c= a ) by A1, A2, A3, Def10;
hence  b in a ; ::_thesis: verum
end;

definition
let A be Ordinal-Sequence;
attrA is Cantor-normal-form  means :Def11: :: ORDINAL5:def 11
( ( for a being ordinal number st a in dom A holds
A . a is Cantor-component ) & ( for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) );
end;

:: deftheorem Def11 defines Cantor-normal-form ORDINAL5:def_11_:_
 for A being Ordinal-Sequence holds
( A is Cantor-normal-form iff ( ( for a being ordinal number st a in dom A holds
A . a is Cantor-component ) & ( for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a) ) ) );

registration
cluster Relation-like Function-like empty T-Sequence-like Ordinal-yielding  ->  Cantor-normal-form for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is empty holds
b1 is Cantor-normal-form
proof
let f be Ordinal-Sequence; ::_thesis: ( f is empty implies f is Cantor-normal-form )
assume A1: f is empty ; ::_thesis: f is Cantor-normal-form
hence  for a being ordinal number st a in dom f holds
f . a is Cantor-component ; :: according to ORDINAL5:def_11 ::_thesis: for a, b being ordinal number st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a)
thus  for a, b being ordinal number st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a) by A1; ::_thesis: verum
end;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding Cantor-normal-form  ->  decreasing for set ;
coherence
 for b1 being Ordinal-Sequence st b1 is Cantor-normal-form holds
b1 is decreasing
proof
let f be Ordinal-Sequence; ::_thesis: ( f is Cantor-normal-form implies f is decreasing )
assume that
 for a being ordinal number st a in dom f holds
f . a is Cantor-component and
A2: for a, b being ordinal number st a in b & b in dom f holds
omega -exponent (f . b) in omega -exponent (f . a) ; :: according to ORDINAL5:def_11 ::_thesis: f is decreasing
let a be ordinal number ; :: according to ORDINAL5:def_1 ::_thesis: for b being ordinal number st a in b & b in dom f holds
f . b in f . a
let b be ordinal number ; ::_thesis: ( a in b & b in dom f implies f . b in f . a )
assume  ( a in b & b in dom f ) ; ::_thesis: f . b in f . a
then  omega -exponent (f . b) in omega -exponent (f . a) by A2;
hence  f . b in f . a by Th63; ::_thesis: verum
end;
end;


theorem :: ORDINAL5:64
for A being Cantor-normal-form Ordinal-Sequence st Sum^ A = 0 holds
A = {}
proof
let A be Cantor-normal-form Ordinal-Sequence; ::_thesis: ( Sum^ A = 0 implies A = {} )
assume A1: ( Sum^ A = 0 & A <> {} ) ; ::_thesis: contradiction
then  0 in dom A by ORDINAL3:8;
then reconsider a = A . 0 as Cantor-component Ordinal by Def11;
 ( 0 in a & a c= Sum^ A ) by Th56, ORDINAL3:8;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th65: :: ORDINAL5:65
for b being ordinal number
for n being Nat st 0 in n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form
proof
let b be ordinal number ; ::_thesis: for n being Nat st 0 in n holds
<%(n *^ (exp (omega,b)))%> is Cantor-normal-form
let n be Nat; ::_thesis: ( 0 in n implies <%(n *^ (exp (omega,b)))%> is Cantor-normal-form )
assume A1: 0 in n ; ::_thesis: <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
set A = <%(n *^ (exp (omega,b)))%>;
A2: ( dom <%(n *^ (exp (omega,b)))%> = 1 & <%(n *^ (exp (omega,b)))%> . 0 = n *^ (exp (omega,b)) ) by AFINSQ_1:def_4;
hereby  :: according to ORDINAL5:def_11 ::_thesis: for a, b being ordinal number st a in b & b in dom <%(n *^ (exp (omega,b)))%> holds
omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a)
let a be ordinal number ; ::_thesis: ( a in dom <%(n *^ (exp (omega,b)))%> implies <%(n *^ (exp (omega,b)))%> . a is Cantor-component )
assume  a in dom <%(n *^ (exp (omega,b)))%> ; ::_thesis: <%(n *^ (exp (omega,b)))%> . a is Cantor-component
then  ( a = 0 & 0 in 1 ) by A2, ORDINAL3:15, TARSKI:def_1;
hence  <%(n *^ (exp (omega,b)))%> . a is Cantor-component by A1, A2, Def9; ::_thesis: verum
end;
let a, b be ordinal number ; ::_thesis: ( a in b & b in dom <%(n *^ (exp (omega,b)))%> implies omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) )
assume A3: a in b ; ::_thesis: ( not b in dom <%(n *^ (exp (omega,b)))%> or omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) )
assume  b in dom <%(n *^ (exp (omega,b)))%> ; ::_thesis: omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a)
hence  omega -exponent (<%(n *^ (exp (omega,b)))%> . b) in omega -exponent (<%(n *^ (exp (omega,b)))%> . a) by A3, A2, ORDINAL3:15, TARSKI:def_1; ::_thesis: verum
end;

registration
cluster Relation-like Function-like non empty T-Sequence-like Ordinal-yielding Cantor-normal-form for set ;
existence
 ex b1 being Ordinal-Sequence st
( not b1 is empty & b1 is Cantor-normal-form )
proof
take A = <%(1 *^ (exp (omega,1)))%>; ::_thesis: ( not A is empty & A is Cantor-normal-form )
thus  not A is empty ; ::_thesis: A is Cantor-normal-form
 0 in 1 by NAT_1:44;
hence  A is Cantor-normal-form by Th65; ::_thesis: verum
end;
end;

theorem Th66: :: ORDINAL5:66
for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
( A is Cantor-normal-form & B is Cantor-normal-form )
proof
let A, B be Ordinal-Sequence; ::_thesis: ( A ^ B is Cantor-normal-form implies ( A is Cantor-normal-form & B is Cantor-normal-form ) )
set AB = A ^ B;
assume that
A1: for a being ordinal number st a in dom (A ^ B) holds
(A ^ B) . a is Cantor-component and
A2: for a, b being ordinal number st a in b & b in dom (A ^ B) holds
omega -exponent ((A ^ B) . b) in omega -exponent ((A ^ B) . a) ; :: according to ORDINAL5:def_11 ::_thesis: ( A is Cantor-normal-form & B is Cantor-normal-form )
A3: dom (A ^ B) = (dom A) +^ (dom B) by ORDINAL4:def_1;
then A4: dom A c= dom (A ^ B) by ORDINAL3:24;
thus  A is Cantor-normal-form ::_thesis: B is Cantor-normal-form
proof
hereby  :: according to ORDINAL5:def_11 ::_thesis: for a, b being ordinal number st a in b & b in dom A holds
omega -exponent (A . b) in omega -exponent (A . a)
let a be ordinal number ; ::_thesis: ( a in dom A implies A . a is Cantor-component )
assume  a in dom A ; ::_thesis: A . a is Cantor-component
then  ( A . a = (A ^ B) . a & a in dom (A ^ B) ) by A4, ORDINAL4:def_1;
hence  A . a is Cantor-component by A1; ::_thesis: verum
end;
let a, b be ordinal number ; ::_thesis: ( a in b & b in dom A implies omega -exponent (A . b) in omega -exponent (A . a) )
assume A5: ( a in b & b in dom A ) ; ::_thesis: omega -exponent (A . b) in omega -exponent (A . a)
then  a in dom A by ORDINAL1:10;
then  ( A . a = (A ^ B) . a & A . b = (A ^ B) . b & b in dom (A ^ B) ) by A4, A5, ORDINAL4:def_1;
hence  omega -exponent (A . b) in omega -exponent (A . a) by A2, A5; ::_thesis: verum
end;
hereby  :: according to ORDINAL5:def_11 ::_thesis: for a, b being ordinal number st a in b & b in dom B holds
omega -exponent (B . b) in omega -exponent (B . a)
let a be ordinal number ; ::_thesis: ( a in dom B implies B . a is Cantor-component )
assume  a in dom B ; ::_thesis: B . a is Cantor-component
then  ( B . a = (A ^ B) . ((dom A) +^ a) & (dom A) +^ a in dom (A ^ B) ) by A3, ORDINAL3:17, ORDINAL4:def_1;
hence  B . a is Cantor-component by A1; ::_thesis: verum
end;
let a, b be ordinal number ; ::_thesis: ( a in b & b in dom B implies omega -exponent (B . b) in omega -exponent (B . a) )
assume A6: ( a in b & b in dom B ) ; ::_thesis: omega -exponent (B . b) in omega -exponent (B . a)
then  a in dom B by ORDINAL1:10;
then  ( B . a = (A ^ B) . ((dom A) +^ a) & B . b = (A ^ B) . ((dom A) +^ b) & (dom A) +^ b in dom (A ^ B) & (dom A) +^ a in (dom A) +^ b ) by A3, A6, ORDINAL3:17, ORDINAL4:def_1;
hence  omega -exponent (B . b) in omega -exponent (B . a) by A2; ::_thesis: verum
end;

theorem :: ORDINAL5:67
for A being Cantor-normal-form Ordinal-Sequence st A <> {} holds
ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
proof
let A be Cantor-normal-form Ordinal-Sequence; ::_thesis: ( A <> {} implies ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B )
assume  A <> {} ; ::_thesis: ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
then consider n being Nat such that
A1: len A = n + 1 by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def_12;
 n + 1 = 1 +^ n by CARD_2:36;
then consider S1, S2 being T-Sequence such that
A2: ( A = S1 ^ S2 & dom S1 = 1 & dom S2 = n ) by A1, Th2;
reconsider S1 = S1, S2 = S2 as Ordinal-Sequence by A2, Th4;
 S1 ^ S2 is Cantor-normal-form by A2;
then reconsider S1 = S1, S2 = S2 as Cantor-normal-form Ordinal-Sequence by Th66;
 0 in 1 by NAT_1:44;
then reconsider c = S1 . 0 as Cantor-component Ordinal by A2, Def11;
take  c ; ::_thesis: ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
take  S2 ; ::_thesis: A = <%c%> ^ S2
 len S1 = 1 by A2;
hence  A = <%c%> ^ S2 by A2, AFINSQ_1:34; ::_thesis: verum
end;

theorem Th68: :: ORDINAL5:68
for A being non empty Cantor-normal-form Ordinal-Sequence
for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds
<%c%> ^ A is Cantor-normal-form
proof
let A be non empty Cantor-normal-form Ordinal-Sequence; ::_thesis: for c being Cantor-component Ordinal st omega -exponent (A . 0) in omega -exponent c holds
<%c%> ^ A is Cantor-normal-form
let c be Cantor-component Ordinal; ::_thesis: ( omega -exponent (A . 0) in omega -exponent c implies <%c%> ^ A is Cantor-normal-form )
assume A1: omega -exponent (A . 0) in omega -exponent c ; ::_thesis: <%c%> ^ A is Cantor-normal-form
set B = <%c%> ^ A;
A2: ( dom <%c%> = 1 & <%c%> . 0 = c ) by AFINSQ_1:def_4;
then A3: dom (<%c%> ^ A) = 1 +^ (dom A) by ORDINAL4:def_1;
hereby  :: according to ORDINAL5:def_11 ::_thesis: for a, b being ordinal number st a in b & b in dom (<%c%> ^ A) holds
omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)
let a be ordinal number ; ::_thesis: ( a in dom (<%c%> ^ A) implies (<%c%> ^ A) . b1 is Cantor-component )
assume A4: a in dom (<%c%> ^ A) ; ::_thesis: (<%c%> ^ A) . b1 is Cantor-component
percases ( a in 1 or ex b being ordinal number st
( b in dom A & a = 1 +^ b ) ) by A3, A4, ORDINAL3:38;
supposeA5: a in 1 ; ::_thesis: (<%c%> ^ A) . b1 is Cantor-component
then  a = 0 by ORDINAL3:15, TARSKI:def_1;
hence  (<%c%> ^ A) . a is Cantor-component by A2, A5, ORDINAL4:def_1; ::_thesis: verum
end;
suppose ex b being ordinal number st
( b in dom A & a = 1 +^ b ) ; ::_thesis: (<%c%> ^ A) . b1 is Cantor-component
then consider b being ordinal number  such that
A6: ( b in dom A & a = 1 +^ b ) ;
 (<%c%> ^ A) . a = A . b by A2, A6, ORDINAL4:def_1;
hence  (<%c%> ^ A) . a is Cantor-component by A6, Def11; ::_thesis: verum
end;
end;
end;
let a, b be ordinal number ; ::_thesis: ( a in b & b in dom (<%c%> ^ A) implies omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) )
assume A7: ( a in b & b in dom (<%c%> ^ A) ) ; ::_thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)
percases ( not a in 1 or a in 1 ) ;
suppose not a in 1 ; ::_thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)
then A8: 1 c= a by ORDINAL1:16;
then A9: ( 1 in b & a in dom (<%c%> ^ A) & (1 +^ (dom A)) -^ 1 = dom A ) by A7, ORDINAL1:10, ORDINAL1:12, ORDINAL3:52;
then A10: ( b -^ 1 in dom A & a -^ 1 in dom A & a -^ 1 in b -^ 1 ) by A8, A3, A7, ORDINAL3:53;
 ( b = 1 +^ (b -^ 1) & a = 1 +^ (a -^ 1) ) by A8, A9, ORDINAL3:51, ORDINAL3:def_5;
then  ( (<%c%> ^ A) . a = A . (a -^ 1) & (<%c%> ^ A) . b = A . (b -^ 1) ) by A2, A10, ORDINAL4:def_1;
hence  omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by A10, Def11; ::_thesis: verum
end;
suppose a in 1 ; ::_thesis: omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a)
then A11: ( (<%c%> ^ A) . a = <%c%> . a & a = 0 ) by A2, ORDINAL3:15, ORDINAL4:def_1, TARSKI:def_1;
then A12: succ 0 c= b by A7, ORDINAL1:21;
then  b -^ 1 in (1 +^ (dom A)) -^ 1 by A3, A7, ORDINAL3:53;
then A13: ( b -^ 1 in dom A & b = 1 +^ (b -^ 1) ) by A12, ORDINAL3:52, ORDINAL3:def_5;
then A14: (<%c%> ^ A) . b = A . (b -^ 1) by A2, ORDINAL4:def_1;
 ( 0 in dom A & ( b -^ 1 = 0 or 0 in b -^ 1 ) ) by ORDINAL3:8;
then  ( omega -exponent (A . 0) = omega -exponent (A . (b -^ 1)) or omega -exponent (A . (b -^ 1)) in omega -exponent (A . 0) ) by A13, Def11;
hence  omega -exponent ((<%c%> ^ A) . b) in omega -exponent ((<%c%> ^ A) . a) by A1, A2, A11, A14, ORDINAL1:10; ::_thesis: verum
end;
end;
end;

theorem :: ORDINAL5:69
for a being ordinal number ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
proof
let a be ordinal number ; ::_thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
defpred S1[ Ordinal] means ( 0 in $1 implies ex A being non empty Cantor-normal-form Ordinal-Sequence st $1 = Sum^ A );
A1: for a being ordinal number st ( for b being ordinal number st b in a holds
S1[b] ) holds
S1[a]
proof
let a be ordinal number ; ::_thesis: ( ( for b being ordinal number st b in a holds
S1[b] ) implies S1[a] )
assume that
A2: for b being ordinal number st b in a holds
S1[b] and
A3: 0 in a ; ::_thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
consider n being Nat, b being ordinal number  such that
A4: ( a = (n *^ (exp (omega,(omega -exponent a)))) +^ b & 0 in n & b in exp (omega,(omega -exponent a)) ) by A3, Th62;
reconsider s = n *^ (exp (omega,(omega -exponent a))) as Cantor-component Ordinal by A4, Def9;
set c = omega -exponent a;
B5: exp (omega,(omega -exponent a)) c= a by A3, Def10;
percases ( b = 0 or 0 in b ) by ORDINAL3:8;
supposeA6: b = 0 ; ::_thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
reconsider A = <%(n *^ (exp (omega,(omega -exponent a))))%> as non empty Cantor-normal-form Ordinal-Sequence by A4, Th65;
take  A ; ::_thesis: a = Sum^ A
thus a = n *^ (exp (omega,(omega -exponent a))) by A4, A6, ORDINAL2:27
.= Sum^ A by Th53 ; ::_thesis: verum
end;
suppose 0 in b ; ::_thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
then consider A being non empty Cantor-normal-form Ordinal-Sequence such that
A7: b = Sum^ A by B5, A2, A4;
A8: A . 0 in exp (omega,(omega -exponent a)) by A4, A7, Th56, ORDINAL1:12;
 0 in dom A by ORDINAL3:8;
then  A . 0 is Cantor-component Ordinal by Def11;
then  0 in A . 0 by ORDINAL3:8;
then  exp (omega,(omega -exponent (A . 0))) c= A . 0 by Def10;
then B9: exp (omega,(omega -exponent (A . 0))) in exp (omega,(omega -exponent a)) by A8, ORDINAL1:12;
 n in omega by ORDINAL1:def_12;
then  omega -exponent s = omega -exponent a by A4, Th58;
then reconsider B = <%s%> ^ A as non empty Cantor-normal-form Ordinal-Sequence by B9, Th68, Th12;
take  B ; ::_thesis: a = Sum^ B
thus  a = Sum^ B by A4, A7, Th55; ::_thesis: verum
end;
end;
end;
A10: for b being ordinal number holds S1[b] from ORDINAL1:sch_2(A1);
percases ( a = 0 or 0 in a ) by ORDINAL3:8;
supposeA11: a = 0 ; ::_thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
reconsider A = {} as Cantor-normal-form Ordinal-Sequence ;
take  A ; ::_thesis: a = Sum^ A
thus  a = Sum^ A by A11, Th52; ::_thesis: verum
end;
suppose 0 in a ; ::_thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
then  ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A by A10;
hence  ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A ; ::_thesis: verum
end;
end;
end;