theorem :: ORDINAL7:59

for a being non empty Ordinal
for n, m being non zero Nat holds CantorNF ((n *^ (exp (omega,a))) +^ m) = <%(n *^ (exp (omega,a))),m%>