( dom f = X & rng f = card X & f is one-to-one ) by ThNum1;
then ( dom (f " ) = card X & rng (f " ) = X & f " is one-to-one ) by FUNCT_1:55;
hence f " is Denumeration of X by ThNum2; :: thesis: verum