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