theorem :: ORDINAL7:62

for a being 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)