let A be Cantor-normal-form Ordinal-Sequence; ( A <> {} implies ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B )
assume
A <> {}
; ex c being Cantor-component Ordinal ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
then consider n being Nat such that
A1:
len A = n + 1
by NAT_1:6;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
n + 1 = 1 +^ n
by CARD_2:36;
then consider S1, S2 being Sequence such that
A2:
( A = S1 ^ S2 & dom S1 = 1 & dom S2 = n )
by A1, Th2;
reconsider S1 = S1, S2 = S2 as Ordinal-Sequence by A2, Th4;
S1 ^ S2 is Cantor-normal-form
by A2;
then reconsider S1 = S1, S2 = S2 as Cantor-normal-form Ordinal-Sequence by Th66;
0 in Segm 1
by NAT_1:44;
then reconsider c = S1 . 0 as Cantor-component Ordinal by A2, Def11;
take
c
; ex B being Cantor-normal-form Ordinal-Sequence st A = <%c%> ^ B
take
S2
; A = <%c%> ^ S2
len S1 = 1
by A2;
hence
A = <%c%> ^ S2
by A2, AFINSQ_1:34; verum