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