dom f = X by Th67;
then A1: rng (f ") = X by FUNCT_1:33;
rng f = X by Def3;
then f " is Function of X,X by Th31;
hence f " is Permutation of X by A1, Th83; :: thesis: verum