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