let X be ordinal-membered set ; :: thesis: rng (numbering X) = X
thus rng (numbering X) = On X by ThN1
.= X by EXCH10 ; :: thesis: verum