theorem Th85: :: ORDINAL7:72

for a, b being Ordinal st ( a <> 0 implies omega -exponent b in omega -exponent (last (CantorNF a)) ) holds
a (+) b = a +^ b