let a, b be Ordinal; :: thesis: dom (CantorNF a) c= dom (CantorNF (a (+) b))
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set C0 = CantorNF (a (+) b);
A1: dom (CantorNF a) = card (dom (omega -exponent (CantorNF a))) by Def1
.= card (rng (omega -exponent (CantorNF a))) by CARD_1:70 ;
card (rng (omega -exponent (CantorNF a))) c= card ((rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))) by XBOOLE_1:7, CARD_1:11;
then card (rng (omega -exponent (CantorNF a))) c= card (rng (omega -exponent (CantorNF (a (+) b)))) by Th76;
then dom (CantorNF a) c= card (dom (omega -exponent (CantorNF (a (+) b)))) by A1, CARD_1:70;
hence dom (CantorNF a) c= dom (CantorNF (a (+) b)) by Def1; :: thesis: verum