let a be non empty Ordinal; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum