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