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