defpred S1[ Nat] means for a being non empty Ordinal st $1 = len (CantorNF a) holds
P1[a];
A3: S1[1]
proof
let a be non empty Ordinal; :: thesis: ( 1 = len (CantorNF a) implies P1[a] )
assume A4: 1 = len (CantorNF a) ; :: thesis: P1[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 P1[a] by A1, A6; :: thesis: verum
end;
A7: for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non zero Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
let a be non empty Ordinal; :: thesis: ( k + 1 = len (CantorNF a) implies P1[a] )
assume A9: k + 1 = len (CantorNF a) ; :: thesis: P1[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;
end;
then P1[a0 (+) (n *^ (exp (omega,b)))] by A2, A8, A12;
then P1[(Sum^ <%c%>) (+) a0] by A11, ORDINAL5:53;
then P1[(Sum^ <%c%>) +^ a0] by A10, Th84;
then P1[c +^ a0] by ORDINAL5:53;
then P1[ Sum^ (<%c%> ^ A0)] by ORDINAL5:55;
hence P1[a] by A10; :: thesis: verum
end;
A18: for k being non zero Nat holds S1[k] from NAT_1:sch 10(A3, A7);
 let a be non empty Ordinal; :: thesis: P1[a]
not len (CantorNF a) is zero ;
hence P1[a] by A18; :: thesis: verum