set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
A1: rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by Th76;
( not 0 in rng (omega -exponent (CantorNF a)) & not 0 in rng (omega -exponent (CantorNF b)) ) by Th92;
then not 0 in rng (omega -exponent (CantorNF (a (+) b))) by A1, XBOOLE_0:def 3;
hence a (+) b is limit_ordinal by Th92; :: thesis: verum