theorem :: ORDINAL7:81

for a, b being Ordinal st rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) holds
for c being Ordinal st c in dom (CantorNF a) holds
(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)