defpred S1[ Nat] means for a being Ordinal
for n being non zero Nat st $1 = n holds
P1[n *^ (exp (omega,a))];
A3: S1[1]
proof
let a be Ordinal; :: thesis: for n being non zero Nat st 1 = n holds
P1[n *^ (exp (omega,a))]
let n be non zero Nat; :: thesis: ( 1 = n implies P1[n *^ (exp (omega,a))] )
assume 1 = n ; :: thesis: P1[n *^ (exp (omega,a))]
then n *^ (exp (omega,a)) = exp (omega,a) by ORDINAL2:39;
hence P1[n *^ (exp (omega,a))] by A1; :: thesis: verum
end;
A4: 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 A5: S1[k] ; :: thesis: S1[k + 1]
let a be Ordinal; :: thesis: for n being non zero Nat st k + 1 = n holds
P1[n *^ (exp (omega,a))]
let n be non zero Nat; :: thesis: ( k + 1 = n implies P1[n *^ (exp (omega,a))] )
assume k + 1 = n ; :: thesis: P1[n *^ (exp (omega,a))]
then n *^ (exp (omega,a)) = (Segm (k + 1)) *^ (exp (omega,a))
.= (succ (Segm k)) *^ (exp (omega,a)) by NAT_1:38
.= (k *^ (exp (omega,a))) +^ (exp (omega,a)) by ORDINAL2:36
.= (k *^ (exp (omega,a))) (+) (exp (omega,a)) by Lm9 ;
hence P1[n *^ (exp (omega,a))] by A2, A5; :: thesis: verum
end;
A7: for k being non zero Nat holds S1[k] from NAT_1:sch 10(A3, A4);
 defpred S2[ Nat] means for a being non empty Ordinal st $1 = len (CantorNF a) holds
P1[a];
A8: S2[1]
proof
let a be non empty Ordinal; :: thesis: ( 1 = len (CantorNF a) implies P1[a] )
assume A9: 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
A10: ( 0 in Segm n & (CantorNF a) . 0 = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
A11: not n is zero by A10;
CantorNF a = <%((CantorNF a) . 0)%> by A9, AFINSQ_1:34;
then Sum^ (CantorNF a) = n *^ (exp (omega,b)) by A10, ORDINAL5:53;
hence P1[a] by A7, A11; :: thesis: verum
end;
defpred S3[ Nat] means for a being Ordinal
for b being non empty Ordinal
for n being non zero Nat st $1 = n & P1[b] holds
P1[b (+) (n *^ (exp (omega,a)))];
A12: S3[1]
proof
let a be Ordinal; :: thesis: for b being non empty Ordinal
for n being non zero Nat st 1 = n & P1[b] holds
P1[b (+) (n *^ (exp (omega,a)))]
let b be non empty Ordinal; :: thesis: for n being non zero Nat st 1 = n & P1[b] holds
P1[b (+) (n *^ (exp (omega,a)))]
let n be non zero Nat; :: thesis: ( 1 = n & P1[b] implies P1[b (+) (n *^ (exp (omega,a)))] )
assume A13: ( 1 = n & P1[b] ) ; :: thesis: P1[b (+) (n *^ (exp (omega,a)))]
then P1[b (+) (exp (omega,a))] by A2;
hence P1[b (+) (n *^ (exp (omega,a)))] by A13, ORDINAL2:39; :: thesis: verum
end;
A14: for k being non zero Nat st S3[k] holds
S3[k + 1]
proof
let k be non zero Nat; :: thesis: ( S3[k] implies S3[k + 1] )
assume A15: S3[k] ; :: thesis: S3[k + 1]
let a be Ordinal; :: thesis: for b being non empty Ordinal
for n being non zero Nat st k + 1 = n & P1[b] holds
P1[b (+) (n *^ (exp (omega,a)))]
let b be non empty Ordinal; :: thesis: for n being non zero Nat st k + 1 = n & P1[b] holds
P1[b (+) (n *^ (exp (omega,a)))]
let n be non zero Nat; :: thesis: ( k + 1 = n & P1[b] implies P1[b (+) (n *^ (exp (omega,a)))] )
assume A16: ( k + 1 = n & P1[b] ) ; :: thesis: P1[b (+) (n *^ (exp (omega,a)))]
then P1[b (+) (k *^ (exp (omega,a)))] by A15;
then P1[(b (+) (k *^ (exp (omega,a)))) (+) (exp (omega,a))] by A2;
then P1[b (+) ((k *^ (exp (omega,a))) (+) (exp (omega,a)))] by Th81;
then P1[b (+) ((k *^ (exp (omega,a))) +^ (exp (omega,a)))] by Lm9;
then P1[b (+) ((succ k) *^ (exp (omega,a)))] by ORDINAL2:36;
hence P1[b (+) (n *^ (exp (omega,a)))] by A16, Lm5; :: thesis: verum
end;
A17: for k being non zero Nat holds S3[k] from NAT_1:sch 10(A12, A14);
 A18: for k being non zero Nat st S2[k] holds
S2[k + 1]
proof
let k be non zero Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume A19: S2[k] ; :: thesis: S2[k + 1]
let a be non empty Ordinal; :: thesis: ( k + 1 = len (CantorNF a) implies P1[a] )
assume A20: k + 1 = len (CantorNF a) ; :: thesis: P1[a]
consider c being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A21: CantorNF a = <%c%> ^ A0 by ORDINAL5:67;
consider b being Ordinal, n being Nat such that
A22: ( 0 in Segm n & c = n *^ (exp (omega,b)) ) by ORDINAL5:def 9;
reconsider n = n as non zero Nat by A22;
A23: k + 1 = (len <%c%>) + (len A0) by A20, A21, AFINSQ_1:17
.= 1 + (len A0) by AFINSQ_1:34 ;
then A0 <> {} ;
then reconsider a0 = Sum^ A0 as non empty Ordinal ;
len (CantorNF a0) = k by A23;
then P1[a0 (+) (n *^ (exp (omega,b)))] by A17, A19;
then P1[(Sum^ <%c%>) (+) a0] by A22, ORDINAL5:53;
then P1[(Sum^ <%c%>) +^ a0] by A21, Th84;
then P1[c +^ a0] by ORDINAL5:53;
then P1[ Sum^ (<%c%> ^ A0)] by ORDINAL5:55;
hence P1[a] by A21; :: thesis: verum
end;
A24: for k being non zero Nat holds S2[k] from NAT_1:sch 10(A8, A18);
 let a be non empty Ordinal; :: thesis: P1[a]
not len (CantorNF a) is zero ;
hence P1[a] by A24; :: thesis: verum