let A be finite Ordinal-Sequence; for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds
Sum^ A in exp (omega,(omega -exponent a))
let a be Ordinal; ( <%a%> ^ A is Cantor-normal-form implies Sum^ A in exp (omega,(omega -exponent a)) )
assume
<%a%> ^ A is Cantor-normal-form
; Sum^ A in exp (omega,(omega -exponent a))
then reconsider B = <%a%> ^ A as Cantor-normal-form Ordinal-Sequence ;
now for c being Ordinal st c in dom A holds
A . c in exp (omega,(omega -exponent a))let c be
Ordinal;
( c in dom A implies A . c in exp (omega,(omega -exponent a)) )assume A1:
c in dom A
;
A . c in exp (omega,(omega -exponent a))then reconsider n =
c as
Nat ;
(len <%a%>) + n in dom B
by A1, AFINSQ_1:23;
then A2:
n + 1
in dom B
by AFINSQ_1:34;
B . ((len <%a%>) + n) = A . n
by A1, AFINSQ_1:def 3;
then A3:
A . n = B . (n + 1)
by AFINSQ_1:34;
0 in Segm (n + 1)
by NAT_1:44;
then
omega -exponent (B . (n + 1)) in omega -exponent (B . 0)
by A2, ORDINAL5:def 11;
then
exp (
omega,
(omega -exponent (A . n)))
in exp (
omega,
(omega -exponent (B . 0)))
by A3, ORDINAL4:24;
then A4:
exp (
omega,
(omega -exponent (A . n)))
in exp (
omega,
(omega -exponent a))
by AFINSQ_1:35;
B . (n + 1) is
Cantor-component
by A2, ORDINAL5:def 11;
then consider b being
Ordinal,
m being
Nat such that A5:
(
0 in Segm m &
A . n = m *^ (exp (omega,b)) )
by A3, ORDINAL5:def 9;
(
0 in m &
m in omega )
by A5, ORDINAL1:def 12;
then
omega -exponent (A . n) = b
by A5, ORDINAL5:58;
hence
A . c in exp (
omega,
(omega -exponent a))
by A4, A5, Th42;
verum end;
hence
Sum^ A in exp (omega,(omega -exponent a))
by Th41; verum