let A be finite Ordinal-Sequence; :: thesis: for a being Ordinal st <%a%> ^ A is Cantor-normal-form holds
Sum^ A in exp (omega,(omega -exponent a))
let a be Ordinal; :: thesis: ( <%a%> ^ A is Cantor-normal-form implies Sum^ A in exp (omega,(omega -exponent a)) )
assume <%a%> ^ A is Cantor-normal-form ; :: thesis: Sum^ A in exp (omega,(omega -exponent a))
then reconsider B = <%a%> ^ A as Cantor-normal-form Ordinal-Sequence ;

now :: thesis: for c being Ordinal st c in dom A holds
A . c in exp (omega,(omega -exponent a))

let c be Ordinal; :: thesis: ( c in dom A implies A . c in exp (omega,(omega -exponent a)) )
assume A1: c in dom A ; :: thesis: 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; :: thesis: verum

end;

hence Sum^ A in exp (omega,(omega -exponent a)) by Th41; :: thesis: verum