for a, b being Ordinal
for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by Th78;