let a, b be Ordinal; :: thesis: a c= a (+) b
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
A1: dom (CantorNF a) c= dom (CantorNF (a (+) b)) by Th77;
for x being object st x in dom (CantorNF a) holds
(CantorNF a) . x c= (CantorNF (a (+) b)) . x by Th98;
then Sum^ (CantorNF a) c= Sum^ (CantorNF (a (+) b)) by A1, Th28;
hence a c= a (+) b ; :: thesis: verum