theorem :: ORDINAL7:80

for a, b being Ordinal
for n being non zero Nat st n *^ (exp (omega,b)) c= a & a in (n + 1) *^ (exp (omega,b)) holds
(CantorNF a) . 0 = n *^ (exp (omega,b))