let a be Ordinal; :: 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 );
A1: for a being Ordinal st ( for b being Ordinal st b in a holds
S₁[b] ) holds
S₁[a]

proof

let a be Ordinal; :: thesis: ( ( for b being Ordinal st b in a holds
S₁[b] ) implies S₁[a] )
assume that
A2: for b being Ordinal st b in a holds
S₁[b] and
A3: 0 in a ; :: thesis: ex A being non empty Cantor-normal-form Ordinal-Sequence st a = Sum^ A
consider n being Nat, b being Ordinal such that
A4: ( a = (n *^ (exp (omega,(omega -exponent a)))) +^ b & 0 in Segm n & b in exp (omega,(omega -exponent a)) ) by A3, Th62;
reconsider s = n *^ (exp (omega,(omega -exponent a))) as Cantor-component Ordinal by A4, Def9;
set c = omega -exponent a;
A5: exp (omega,(omega -exponent a)) c= a by A3, Def10;

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

suppose A6: 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 A4, Th65;
take A ; :: thesis: a = Sum^ A
thus a = n *^ (exp (omega,(omega -exponent a))) by A4, A6, ORDINAL2:27
.= Sum^ A by Th53 ; :: 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
A7: b = Sum^ A by A5, A2, A4;
A8: A . 0 in exp (omega,(omega -exponent a)) by A4, A7, Th56, ORDINAL1:12;
0 in dom A by ORDINAL3:8;
then A . 0 is Cantor-component Ordinal by Def11;
then 0 in A . 0 by ORDINAL3:8;
then exp (omega,(omega -exponent (A . 0))) c= A . 0 by Def10;
then A9: exp (omega,(omega -exponent (A . 0))) in exp (omega,(omega -exponent a)) by A8, ORDINAL1:12;
n in omega by ORDINAL1:def 12;
then omega -exponent s = omega -exponent a by A4, Th58;
then reconsider B = <%s%> ^ A as non empty Cantor-normal-form Ordinal-Sequence by A9, Th68, Th12;
take B ; :: thesis: a = Sum^ B
thus a = Sum^ B by A4, A7, Th55; :: thesis: verum

end;

end;

end;

A10: for b being Ordinal holds S₁[b] from ORDINAL1:sch 2(A1);

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

suppose A11: 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 A11, Th52; :: 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 A10;
hence ex A being Cantor-normal-form Ordinal-Sequence st a = Sum^ A ; :: thesis: verum

end;

end;