theorem Th77: :: ORDINAL7:64

for a, b being Ordinal holds dom (CantorNF a) c= dom (CantorNF (a (+) b))