:: Epsilon Numbers and Cantor Normal Form
:: by Grzegorz Bancerek
::
:: Received October 20, 2009
:: Copyright (c) 2009-2012 Association of Mizar Users


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 )
proofend;

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
proofend;
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 )
proofend;
end;

registration
let f be T-Sequence;
let g be non empty T-Sequence;
clusterf ^ g ->  non empty ;
coherence
 not f ^ g is empty
proofend;
clusterg ^ f ->  non empty ;
coherence
 not g ^ f is empty
proofend;
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 )
proofend;

theorem Th3: :: ORDINAL5:3
for S1, S2 being T-Sequence holds
( rng S1 c= rng (S1 ^ S2) & rng S2 c= rng (S1 ^ S2) )
proofend;

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 )
proofend;

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
proofend;
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
proofend;
end;

theorem Th5: :: ORDINAL5:5
for f being T-Sequence holds
( f is infinite iff omega c= dom f )
proofend;

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
proofend;
cluster empty  ->  empty increasing decreasing for set ;
coherence
 for b1 being empty set holds
( b1 is decreasing & b1 is increasing )
proofend;
end;

registration
let a be ordinal number ;
cluster<%a%> ->  Ordinal-yielding ;
coherence
 <%a%> is Ordinal-yielding
proofend;
end;

registration
let a be ordinal number ;
cluster<%a%> ->  increasing decreasing ;
coherence
 ( <%a%> is decreasing &amp; <%a%> is increasing )
proofend;
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 &amp; b1 is increasing &amp; b1 is non-decreasing &amp; b1 is non-increasing &amp; b1 is finite &amp; not b1 is empty )
proofend;
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
proofend;

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)
proofend;

theorem Th8: :: ORDINAL5:8
for a being ordinal number
for f being Ordinal-Sequence st 0 in a &amp; ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is non-decreasing
proofend;

theorem Th9: :: ORDINAL5:9
for a, b being ordinal number st a is limit_ordinal &amp; 0 in b holds
exp (a,b) is limit_ordinal
proofend;

theorem :: ORDINAL5:10
for a being ordinal number
for f being Ordinal-Sequence st 1 in a &amp; ( for b being ordinal number st b in dom f holds
f . b = exp (a,b) ) holds
f is increasing
proofend;

theorem Th11: :: ORDINAL5:11
for a, b being ordinal number
for x being set st 0 in a &amp; not b is empty &amp; b is limit_ordinal holds
( x in exp (a,b) iff ex c being ordinal number st
( c in b &amp; x in exp (a,c) ) )
proofend;

theorem Th12: :: ORDINAL5:12
for a, b, c being ordinal number st 0 in a &amp; exp (a,b) in exp (a,c) holds
b in c
proofend;

begin

definition
let a, b be Ordinal;
funca |^|^ b ->  Ordinal means :Def4: :: ORDINAL5:def 4
 ex phi being Ordinal-Sequence st
( it = last phi &amp; dom phi = succ b &amp; phi . {} = 1 &amp; ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) &amp; ( for c being Ordinal st c in succ b &amp; c <> {} &amp; 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 &amp; dom phi = succ b &amp; phi . {} = 1 &amp; ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) &amp; ( for c being Ordinal st c in succ b &amp; c <> {} &amp; 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 &amp; dom phi = succ b &amp; phi . {} = 1 &amp; ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) &amp; ( for c being Ordinal st c in succ b &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) &amp; ex phi being Ordinal-Sequence st
( b2 = last phi &amp; dom phi = succ b &amp; phi . {} = 1 &amp; ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) &amp; ( for c being Ordinal st c in succ b &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2;
proofend;
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 &amp; dom phi = succ b &amp; phi . {} = 1 &amp; ( for c being Ordinal st succ c in succ b holds
phi . (succ c) = exp (a,(phi . c)) ) &amp; ( for c being Ordinal st c in succ b &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th13: :: ORDINAL5:13
for a being ordinal number holds a |^|^ 0 = 1
proofend;

theorem Th14: :: ORDINAL5:14
for a, b being ordinal number holds a |^|^ (succ b) = exp (a,(a |^|^ b))
proofend;

theorem Th15: :: ORDINAL5:15
for b, a being ordinal number st b <> {} &amp; b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b &amp; ( for c being ordinal number st c in b holds
phi . c = a |^|^ c ) holds
a |^|^ b = lim phi
proofend;

theorem Th16: :: ORDINAL5:16
for a being ordinal number holds a |^|^ 1 = a
proofend;

theorem Th17: :: ORDINAL5:17
for a being ordinal number holds 1 |^|^ a = 1
proofend;

theorem Th18: :: ORDINAL5:18
for a being ordinal number holds a |^|^ 2 = exp (a,a)
proofend;

theorem :: ORDINAL5:19
for a being ordinal number holds a |^|^ 3 = exp (a,(exp (a,a)))
proofend;

theorem :: ORDINAL5:20
for n being Nat holds
( 0 |^|^ (2 * n) = 1 &amp; 0 |^|^ ((2 * n) + 1) = 0 )
proofend;

theorem Th21: :: ORDINAL5:21
for a, b, c being ordinal number st a c= b &amp; 0 in c holds
c |^|^ a c= c |^|^ b
proofend;

theorem :: ORDINAL5:22
for a being ordinal number
for f being Ordinal-Sequence st 0 in a &amp; ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is non-decreasing
proofend;

theorem Th23: :: ORDINAL5:23
for a, b being ordinal number st 0 in a &amp; 0 in b holds
a c= a |^|^ b
proofend;

theorem Th24: :: ORDINAL5:24
for a being ordinal number
for m, n being Nat st 1 in a &amp; m < n holds
a |^|^ m in a |^|^ n
proofend;

:: theorem :: false a |^|^ succ omega = a |^|^ omega for a > 0
:: 1 in c &amp; a in b implies c |^|^ a in c |^|^ b
theorem Th25: :: ORDINAL5:25
for a being ordinal number
for f being Ordinal-Sequence st 1 in a &amp; dom f c= omega &amp; ( for b being ordinal number st b in dom f holds
f . b = a |^|^ b ) holds
f is increasing
proofend;

theorem Th26: :: ORDINAL5:26
for a, b being ordinal number st 1 in a &amp; 1 in b holds
a in a |^|^ b
proofend;

theorem Th27: :: ORDINAL5:27
for n, k being Nat holds exp (n,k) = n |^ k
proofend;

registration
let n, k be Nat;
cluster exp (n,k) ->  natural ;
coherence
 exp (n,k) is natural
proofend;
end;

registration
let n, k be Nat;
clustern |^|^ k ->  natural ;
coherence
 n |^|^ k is natural
proofend;
end;

theorem Th28: :: ORDINAL5:28
for n, k being Nat st n > 1 holds
n |^|^ k > k
proofend;

theorem :: ORDINAL5:29
for n being Nat st n > 1 holds
n |^|^ omega = omega
proofend;

theorem Th30: :: ORDINAL5:30
for a being ordinal number st 1 in a holds
a |^|^ omega is limit_ordinal
proofend;

theorem Th31: :: ORDINAL5:31
for a being ordinal number st 0 in a holds
exp (a,(a |^|^ omega)) = a |^|^ omega
proofend;

theorem :: ORDINAL5:32
for a, b being ordinal number st 0 in a &amp; omega c= b holds
a |^|^ b = a |^|^ omega
proofend;

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() &amp; F3((Union F2())) = Union F2() &amp; ( for b being ordinal number st F1() c= b &amp; 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 &amp; a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a &amp; ( 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 &amp; F2() . 0 = F1() ) and
A4: for a being ordinal number st a in omega holds
F2() . (succ a) = F3((F2() . a))
proofend;

scheme :: ORDINAL5:sch 2
CriticalNumber3{ F1() ->  Ordinal, F2( Ordinal) ->  Ordinal } :
 ex a being ordinal number st
( F1() in a &amp; 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 &amp; a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a &amp; ( for b being ordinal number st b in a holds
phi . b = F2(b) ) holds
F2(a) is_limes_of phi
proofend;

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 &amp; b is epsilon )
proofend;

registration
cluster epsilon-transitive epsilon-connected ordinal epsilon for set ;
existence
 ex b1 being ordinal number st b1 is epsilon
proofend;
end;

definition
let a be Ordinal;
func first_epsilon_greater_than a ->  epsilon Ordinal means :Def6: :: ORDINAL5:def 6
( a in it &amp; ( for b being epsilon Ordinal st a in b holds
it c= b ) );
existence
 ex b1 being epsilon Ordinal st
( a in b1 &amp; ( for b being epsilon Ordinal st a in b holds
b1 c= b ) )
proofend;
uniqueness
 for b1, b2 being epsilon Ordinal st a in b1 &amp; ( for b being epsilon Ordinal st a in b holds
b1 c= b ) &amp; a in b2 &amp; ( for b being epsilon Ordinal st a in b holds
b2 c= b ) holds
b1 = b2
proofend;
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 &amp; ( 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
proofend;

theorem :: ORDINAL5:35
for a, b being ordinal number st a in b &amp; b in first_epsilon_greater_than a holds
first_epsilon_greater_than b = first_epsilon_greater_than a
proofend;

theorem Th36: :: ORDINAL5:36
first_epsilon_greater_than 0 = omega |^|^ omega
proofend;

theorem Th37: :: ORDINAL5:37
for e being epsilon Ordinal holds omega in e
proofend;

registration
cluster ordinal epsilon  ->  non empty limit_ordinal for set ;
coherence
 for b1 being Ordinal st b1 is epsilon holds
( not b1 is empty &amp; b1 is limit_ordinal )
proofend;
end;

theorem Th38: :: ORDINAL5:38
for e being epsilon Ordinal holds exp (omega,(exp (e,omega))) = exp (e,(exp (e,omega)))
proofend;

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)))
proofend;

theorem Th40: :: ORDINAL5:40
for e being epsilon Ordinal holds first_epsilon_greater_than e = e |^|^ omega
proofend;

definition
let a be Ordinal;
:: equals omega |^|^ exp(omega, 1+^a); :: wg wikipedii, ale to nie prawda
func epsilon_ a ->  Ordinal means :Def7: :: ORDINAL5:def 7
 ex phi being Ordinal-Sequence st
( it = last phi &amp; dom phi = succ a &amp; phi . {} = omega |^|^ omega &amp; ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) &amp; ( for c being Ordinal st c in succ a &amp; c <> {} &amp; 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 &amp; dom phi = succ a &amp; phi . {} = omega |^|^ omega &amp; ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) &amp; ( for c being Ordinal st c in succ a &amp; c <> {} &amp; 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 &amp; dom phi = succ a &amp; phi . {} = omega |^|^ omega &amp; ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) &amp; ( for c being Ordinal st c in succ a &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) &amp; ex phi being Ordinal-Sequence st
( b2 = last phi &amp; dom phi = succ a &amp; phi . {} = omega |^|^ omega &amp; ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) &amp; ( for c being Ordinal st c in succ a &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) holds
b1 = b2;
proofend;
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 &amp; dom phi = succ a &amp; phi . {} = omega |^|^ omega &amp; ( for b being Ordinal st succ b in succ a holds
phi . (succ b) = (phi . b) |^|^ omega ) &amp; ( for c being Ordinal st c in succ a &amp; c <> {} &amp; c is limit_ordinal holds
phi . c = lim (phi | c) ) ) );

theorem Th41: :: ORDINAL5:41
epsilon_ 0 = omega |^|^ omega
proofend;

theorem Th42: :: ORDINAL5:42
for a being ordinal number holds epsilon_ (succ a) = (epsilon_ a) |^|^ omega
proofend;

theorem Th43: :: ORDINAL5:43
for b being ordinal number st b <> {} &amp; b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b &amp; ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = lim phi
proofend;

theorem Th44: :: ORDINAL5:44
for a, b being ordinal number st a in b holds
epsilon_ a in epsilon_ b
proofend;

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
proofend;

theorem Th46: :: ORDINAL5:46
for b being ordinal number st b <> {} &amp; b is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = b &amp; ( for c being ordinal number st c in b holds
phi . c = epsilon_ c ) holds
epsilon_ b = Union phi
proofend;

theorem Th47: :: ORDINAL5:47
for b being ordinal number
for x being set st not b is empty &amp; b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b &amp; x in epsilon_ c ) )
proofend;

theorem Th48: :: ORDINAL5:48
for a being ordinal number holds a c= epsilon_ a
proofend;

theorem Th49: :: ORDINAL5:49
for X being non empty set st ( for x being set st x in X holds
( x is epsilon Ordinal &amp; ex e being epsilon Ordinal st
( x in e &amp; e in X ) ) ) holds
union X is epsilon Ordinal
proofend;

theorem Th50: :: ORDINAL5:50
for X being non empty set st ( for x being set st x in X holds
x is epsilon Ordinal ) &amp; ( for a being ordinal number st a in X holds
first_epsilon_greater_than a in X ) holds
union X is epsilon Ordinal
proofend;

registration
let a be ordinal number ;
cluster epsilon_ a ->  epsilon ;
coherence
 epsilon_ a is epsilon
proofend;
end;

:: [WP: ] The_ordinal_indexing_of_epsilon_numbers
theorem :: ORDINAL5:51
for a being ordinal number st a is epsilon holds
ex b being ordinal number st a = epsilon_ b
proofend;

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 &amp; dom f = succ (dom A) &amp; f . 0 = 0 &amp; ( 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 &amp; dom f = succ (dom A) &amp; f . 0 = 0 &amp; ( 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 &amp; dom f = succ (dom A) &amp; f . 0 = 0 &amp; ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) &amp; ex f being Ordinal-Sequence st
( b2 = last f &amp; dom f = succ (dom A) &amp; f . 0 = 0 &amp; ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) holds
b1 = b2;
proofend;
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 &amp; dom f = succ (dom A) &amp; f . 0 = 0 &amp; ( for n being Nat st n in dom A holds
f . (n + 1) = (f . n) +^ (A . n) ) ) );

theorem Th52: :: ORDINAL5:52
Sum^ {} = 0
proofend;

theorem Th53: :: ORDINAL5:53
for a being ordinal number holds Sum^ <%a%> = a
proofend;

theorem Th54: :: ORDINAL5:54
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (A ^ <%a%>) = (Sum^ A) +^ a
proofend;

theorem Th55: :: ORDINAL5:55
for a being ordinal number
for A being finite Ordinal-Sequence holds Sum^ (<%a%> ^ A) = a +^ (Sum^ A)
proofend;

theorem Th56: :: ORDINAL5:56
for A being finite Ordinal-Sequence holds A . 0 c= Sum^ A
proofend;

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 &amp; 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 &amp; 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
proofend;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal Cantor-component for set ;
existence
 ex b1 being Ordinal st b1 is Cantor-component
proofend;
end;

definition
let a, b be ordinal number ;
funcb -exponent a ->  Ordinal means :Def10: :: ORDINAL5:def 10
( exp (b,it) c= a &amp; ( for c being ordinal number st exp (b,c) c= a holds
c c= it ) ) if ( 1 in b &amp; 0 in a )
otherwise it = 0 ;
existence
 ( ( 1 in b &amp; 0 in a implies ex b1 being Ordinal st
( exp (b,b1) c= a &amp; ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) ) ) &amp; ( ( not 1 in b or not 0 in a ) implies ex b1 being Ordinal st b1 = 0 ) )
proofend;
uniqueness
 for b1, b2 being Ordinal holds
( ( 1 in b &amp; 0 in a &amp; exp (b,b1) c= a &amp; ( for c being ordinal number st exp (b,c) c= a holds
c c= b1 ) &amp; exp (b,b2) c= a &amp; ( for c being ordinal number st exp (b,c) c= a holds
c c= b2 ) implies b1 = b2 ) &amp; ( ( not 1 in b or not 0 in a ) &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) )
proofend;
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 &amp; 0 in a implies ( b3 = b -exponent a iff ( exp (b,b3) c= a &amp; ( for c being ordinal number st exp (b,c) c= a holds
c c= b3 ) ) ) ) &amp; ( ( 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)))
proofend;

theorem Th58: :: ORDINAL5:58
for b, a being ordinal number
for n being Nat st 0 in n &amp; n in b holds
b -exponent (n *^ (exp (b,a))) = a
proofend;

theorem Th59: :: ORDINAL5:59
for a, b, c being ordinal number st 0 in a &amp; 1 in b &amp; c = b -exponent a holds
a div^ (exp (b,c)) in b
proofend;

theorem Th60: :: ORDINAL5:60
for a, b, c being ordinal number st 0 in a &amp; 1 in b &amp; c = b -exponent a holds
0 in a div^ (exp (b,c))
proofend;

theorem Th61: :: ORDINAL5:61
for b, a, c being ordinal number st b <> 0 holds
a mod^ (exp (b,c)) in exp (b,c)
proofend;

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 &amp; 0 in n &amp; c in exp (omega,(omega -exponent a)) )
proofend;

theorem Th63: :: ORDINAL5:63
for c, b, a being ordinal number st 1 in c &amp; c -exponent b in c -exponent a holds
b in a
proofend;

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 ) &amp; ( for a, b being ordinal number st a in b &amp; 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 ) &amp; ( for a, b being ordinal number st a in b &amp; 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
proofend;
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
proofend;
end;

theorem :: ORDINAL5:64
for A being Cantor-normal-form Ordinal-Sequence st Sum^ A = 0 holds
A = {}
proofend;

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
proofend;

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 &amp; b1 is Cantor-normal-form )
proofend;
end;

theorem Th66: :: ORDINAL5:66
for A, B being Ordinal-Sequence st A ^ B is Cantor-normal-form holds
( A is Cantor-normal-form &amp; B is Cantor-normal-form )
proofend;

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
proofend;

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
proofend;

:: [WP: ] Existence_of_Cantor_Normal_Form_for_ordinal_numbers
theorem :: ORDINAL5:69
for a being ordinal number ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
proofend;