let A be Cantor-normal-form Ordinal-Sequence; :: thesis:
assume A <> {} ; :: thesis:
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:

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

end;

let b, c be Ordinal; :: thesis:
assume A6: ( b in c & c in dom B ) ; :: thesis:
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:

end;

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