for X being set holds
( dom (numbering X) = ord-type X & rng (numbering X) = On X )