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