let X be finite set ; card { F where F is Function of X,X : F is Permutation of X } = (card X) !
set F1 = { F where F is Function of X,X : F is one-to-one } ;
set F2 = { F where F is Function of X,X : F is Permutation of X } ;
A1:
{ F where F is Function of X,X : F is one-to-one } c= { F where F is Function of X,X : F is Permutation of X }
((card X) -' (card X)) ! = 1
by NEWTON:12, XREAL_1:232;
then A4:
((card X) !) / (((card X) -' (card X)) !) = (card X) !
;
{ F where F is Function of X,X : F is Permutation of X } c= { F where F is Function of X,X : F is one-to-one }
then
{ F where F is Function of X,X : F is one-to-one } = { F where F is Function of X,X : F is Permutation of X }
by A1;
hence
card { F where F is Function of X,X : F is Permutation of X } = (card X) !
by A4, Th6; verum