theorem Th86: :: ORDINAL7:73

for a, b being Ordinal
for n being Nat st ( a <> 0 implies b c= omega -exponent (last (CantorNF a)) ) holds
a (+) (n *^ (exp (omega,b))) = a +^ (n *^ (exp (omega,b)))