let a be ordinal number ; :: thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A
defpred S₁[ Ordinal] means ( 0 in $1 implies ex A being non empty Cantor-normal-form Ordinal-Sequence st $1 = Sum^ A );
A0: for a being ordinal number st ( for b being ordinal number st b in a holds
S₁[b] ) holds
S₁[a]

proof

let a be ordinal number ; :: thesis: ( ( for b being ordinal number st b in a holds
S₁[b] ) implies S₁[a] )
assume that
Z0: for b being ordinal number st b in a holds
S₁[b] and
Z1: 0 in a ; :: thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
consider n being natural number , b being ordinal number such that
Z2: ( a = (n *^ (exp omega ,(omega -exponent a))) +^ b & 0 in n & b in exp omega ,(omega -exponent a) ) by Z1, Th43;
reconsider s = n *^ (exp omega ,(omega -exponent a)) as Cantor-component Ordinal by Z2, CC;
set c = omega -exponent a;
exp omega ,(omega -exponent a) c= a by Z1, EXP;
then Z3: S₁[b] by Z0, Z2;

per cases ( b = 0 or 0 in b ) by ORDINAL3:10;

suppose B1: b = 0 ; :: thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A

reconsider A = <%(n *^ (exp omega ,(omega -exponent a)))%> as non empty Cantor-normal-form Ordinal-Sequence by Z2, Th44;
take A ; :: thesis: a = Sum^ A
thus a = n *^ (exp omega ,(omega -exponent a)) by Z2, B1, ORDINAL2:44
.= Sum^ A by Th51 ; :: thesis: verum

end;

suppose 0 in b ; :: thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A

then consider A being non empty Cantor-normal-form Ordinal-Sequence such that
B3: b = Sum^ A by Z3;
B4: A . 0 in exp omega ,(omega -exponent a) by Z2, B3, ORDINAL1:22, Th53;
0 in dom A by ORDINAL3:10;
then A . 0 is Cantor-component Ordinal by CNF;
then 0 in A . 0 by ORDINAL3:10;
then exp omega ,(omega -exponent (A . 0 )) c= A . 0 by EXP;
then exp omega ,(omega -exponent (A . 0 )) in exp omega ,(omega -exponent a) by B4, ORDINAL1:22;
then B5: omega -exponent (A . 0 ) in omega -exponent a by Th006;
n in omega by ORDINAL1:def 13;
then omega -exponent s = omega -exponent a by Z2, Th42;
then reconsider B = <%s%> ^ A as non empty Cantor-normal-form Ordinal-Sequence by B5, Th45;
take B ; :: thesis: a = Sum^ B
thus a = Sum^ B by Z2, B3, Th52; :: thesis: verum

end;

end;

end;

A1: for b being ordinal number holds S₁[b] from ORDINAL1:sch 2(A0);

per cases ( a = 0 or 0 in a ) by ORDINAL3:10;

suppose Y0: a = 0 ; :: thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A

reconsider A = {} as Cantor-normal-form Ordinal-Sequence ;
take A ; :: thesis: a = Sum^ A
thus a = Sum^ A by Y0, Th50; :: thesis: verum

end;

suppose 0 in a ; :: thesis: ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A

then ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A by A1;
hence ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A ; :: thesis: verum

end;

end;