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