let a be non empty Ordinal; for b being Ordinal
for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
let b be Ordinal; for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
let n be non zero Nat; ( b in omega -exponent (last (CantorNF a)) implies CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%> )
assume A1:
b in omega -exponent (last (CantorNF a))
; CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
set A = CantorNF a;
set B = <%(n *^ (exp (omega,b)))%>;
A2:
(CantorNF a) ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form
by A1, Th37;
Sum^ ((CantorNF a) ^ <%(n *^ (exp (omega,b)))%>) =
(Sum^ (CantorNF a)) +^ (n *^ (exp (omega,b)))
by ORDINAL5:54
.=
a +^ (n *^ (exp (omega,b)))
;
hence
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
by A2; verum