theorem Th69: :: ORDINAL7:56

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