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