theorem Th78: :: ORDINAL7:65

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 a))) \ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))