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