let A be Cantor-normal-form Ordinal-Sequence; :: thesis: ( A <> {} implies ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%> )
assume A <> {} ; :: thesis: ex B being Cantor-normal-form Ordinal-Sequence ex a being Cantor-component Ordinal st A = B ^ <%a%>
then consider B being XFinSequence, a being object such that
A1: A = B ^ <%a%> by AFINSQ_1:40;
reconsider B = B as finite Ordinal-Sequence by A1, Th10;
<%a%> is Ordinal-Sequence by A1, Th10;
then consider c being Ordinal such that
A2: rng <%a%> c= c by ORDINAL2:def 4;
{a} c= c by A2, AFINSQ_1:33;
then a in c by ZFMISC_1:31;
then reconsider a = a as Ordinal ;
len A = (len B) + (len <%a%>) by A1, AFINSQ_1:17
.= Segm ((len B) + 1) by AFINSQ_1:34
.= succ (Segm (len B)) by NAT_1:38
.= succ (len B) ;
then len B in len A by ORDINAL1:6;
then A . (len B) is Cantor-component by ORDINAL5:def 11;
then reconsider a = a as Cantor-component Ordinal by A1, AFINSQ_1:36;
dom B c= (dom B) +^ (dom <%a%>) by ORDINAL3:24;
then A3: dom B c= dom A by A1, ORDINAL4:def 1;

A4: now :: thesis: for b being Ordinal st b in dom B holds
B . b is Cantor-component

let b be Ordinal; :: thesis: ( b in dom B implies B . b is Cantor-component )
assume A5: b in dom B ; :: thesis: B . b is Cantor-component
then A . b = B . b by A1, ORDINAL4:def 1;
hence B . b is Cantor-component by A3, A5, ORDINAL5:def 11; :: thesis: verum

end;

now :: thesis: for b, c being Ordinal st b in c & c in dom B holds
omega -exponent (B . c) in omega -exponent (B . b)

let b, c be Ordinal; :: thesis: ( b in c & c in dom B implies omega -exponent (B . c) in omega -exponent (B . b) )
assume A6: ( b in c & c in dom B ) ; :: thesis: omega -exponent (B . c) in omega -exponent (B . b)
then ( b in dom B & c in dom B ) by ORDINAL1:10;
then ( A . b = B . b & A . c = B . c ) by A1, ORDINAL4:def 1;
hence omega -exponent (B . c) in omega -exponent (B . b) by A3, A6, ORDINAL5:def 11; :: thesis: verum

end;

then reconsider B = B as Cantor-normal-form Ordinal-Sequence by A4, ORDINAL5:def 11;
take B ; :: thesis: ex a being Cantor-component Ordinal st A = B ^ <%a%>
take a ; :: thesis: A = B ^ <%a%>
thus A = B ^ <%a%> by A1; :: thesis: verum