let X be set ; :: thesis: card (dom (numbering X)) = card (On X)
( dom (numbering X) = ord-type X & ex a being Ordinal st On X c= a ) by Th18, Def1;
hence card (dom (numbering X)) = card (On X) by CARD_5:7; :: thesis: verum