theorem :: ORDINAL7:61

for a being non empty Ordinal
for n being non zero Nat st omega -exponent (last (CantorNF a)) <> 0 holds
CantorNF (a +^ n) = (CantorNF a) ^ <%n%>