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]
A4:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume A5:
S1[
k]
;
S1[k + 1]
let a be
Ordinal;
for n being non zero Nat st k + 1 = n holds
P1[n *^ (exp (omega,a))]let n be non
zero Nat;
( k + 1 = n implies P1[n *^ (exp (omega,a))] )
assume
k + 1
= n
;
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;
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]
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]
A14:
for k being non zero Nat st S3[k] holds
S3[k + 1]
proof
let k be non
zero Nat;
( S3[k] implies S3[k + 1] )
assume A15:
S3[
k]
;
S3[k + 1]
let a be
Ordinal;
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;
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;
( k + 1 = n & P1[b] implies P1[b (+) (n *^ (exp (omega,a)))] )
assume A16:
(
k + 1
= n &
P1[
b] )
;
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;
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]
A24:
for k being non zero Nat holds S2[k]
from NAT_1:sch 10(A8, A18);
let a be non empty Ordinal; P1[a]
not len (CantorNF a) is zero
;
hence
P1[a]
by A24; verum