theorem Th76: :: ORDINAL7:63

for a, b being Ordinal holds rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))