rng f = card X by Th6;
then A1: dom (f ") = card X by FUNCT_1:33;
dom f = X by Th6;
then rng (f ") = X by FUNCT_1:33;
hence f " is Denumeration of X by A1, Th7; :: thesis: verum