defpred S₁[ Nat] means for a being non empty Ordinal st $1 = len (CantorNF a) holds
P₁[a];
A3: S₁[1]

proof

let a be non empty Ordinal; :: thesis: ( 1 = len (CantorNF a) implies P₁[a] )
assume A4: 1 = len (CantorNF a) ; :: thesis: P₁[a]
then 0 in dom (CantorNF a) by CARD_1:49, TARSKI:def 1;
then (CantorNF a) . 0 is Cantor-component by ORDINAL5:def 11;
then consider b being Ordinal, n being Nat such that
A5: ( 0 in Segm n & (CantorNF a) . 0 = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
A6: not n is zero by A5;
CantorNF a = <%((CantorNF a) . 0)%> by A4, AFINSQ_1:34;
then Sum^ (CantorNF a) = n *^ (exp (omega,b)) by A5, ORDINAL5:53;
hence P₁[a] by A1, A6; :: thesis: verum

end;

A7: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
let a be non empty Ordinal; :: thesis: ( k + 1 = len (CantorNF a) implies P₁[a] )
assume A9: k + 1 = len (CantorNF a) ; :: thesis: P₁[a]
consider c being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A10: CantorNF a = <%c%> ^ A0 by ORDINAL5:67;
consider b being Ordinal, n being Nat such that
A11: ( 0 in Segm n & c = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
reconsider n = n as non zero Nat by A11;
k + 1 = (len <%c%>) + (len A0) by A9, A10, AFINSQ_1:17
.= 1 + (len A0) by AFINSQ_1:34 ;
then A12: len A0 = k ;
then A0 <> {} ;
then reconsider a0 = Sum^ A0 as non empty Ordinal ;
not b in rng (omega -exponent (CantorNF a0))

proof

( 0 in n & n in omega ) by A11, ORDINAL1:def 12;
then omega -exponent c = b by A11, ORDINAL5:58;
then A13: Sum^ A0 in exp (omega,b) by A10, Th43;
A0 <> {} by A12;
then 0 c< Sum^ A0 by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in Sum^ A0 by ORDINAL1:11;
then omega -exponent (Sum^ A0) in b by A13, Th23;
then A14: omega -exponent (A0 . 0) in b by Th44;
assume b in rng (omega -exponent (CantorNF a0)) ; :: thesis: contradiction
then consider x being object such that
A15: ( x in dom (omega -exponent A0) & (omega -exponent A0) . x = b ) by FUNCT_1:def 3;
reconsider x = x as Ordinal by A15;
A16: x in dom A0 by A15, Def1;
then A17: b = omega -exponent (A0 . x) by A15, Def1;

per cases ( x = 0 or x <> 0 ) ;

suppose x = 0 ; :: thesis: contradiction

hence contradiction by A14, A17; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: contradiction

then 0 c< x by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in x by ORDINAL1:11;
hence contradiction by A14, A16, A17, ORDINAL5:def 11; :: thesis: verum

end;

end;

end;

then P₁[a0 (+) (n *^ (exp (omega,b)))] by A2, A8, A12;
then P₁[(Sum^ <%c%>) (+) a0] by A11, ORDINAL5:53;
then P₁[(Sum^ <%c%>) +^ a0] by A10, Th84;
then P₁[c +^ a0] by ORDINAL5:53;
then P₁[ Sum^ (<%c%> ^ A0)] by ORDINAL5:55;
hence P₁[a] by A10; :: thesis: verum

end;

A18: for k being non zero Nat holds S₁[k] from NAT_1:sch 10(A3, A7);
let a be non empty Ordinal; :: thesis: P₁[a]
not len (CantorNF a) is zero ;
hence P₁[a] by A18; :: thesis: verum