let X be finite set ; :: thesis: 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 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Function of X,X : F is one-to-one } or x in { F where F is Function of X,X : F is Permutation of X } )
assume A2: x in { F where F is Function of X,X : F is one-to-one } ; :: thesis: x in { F where F is Function of X,X : F is Permutation of X }
consider F being Function of X,X such that
A3: ( x = F & F is one-to-one ) by A2;
card X = card X ;
then F is onto by A3, STIRL2_1:70;
then F is bijective by A3;
hence x in { F where F is Function of X,X : F is Permutation of X } by A3; :: thesis: verum

end;

{ 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 }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Function of X,X : F is Permutation of X } or x in { F where F is Function of X,X : F is one-to-one } )
assume A4: x in { F where F is Function of X,X : F is Permutation of X } ; :: thesis: x in { F where F is Function of X,X : F is one-to-one }
ex F being Function of X,X st
( x = F & F is Permutation of X ) by A4;
hence x in { F where F is Function of X,X : F is one-to-one } ; :: thesis: verum

end;

then A5: { 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, XBOOLE_0:def 10;
((card X) -' (card X)) ! = 1 by NEWTON:18, XREAL_1:234;
then ((card X) ! ) / (((card X) -' (card X)) ! ) = (card X) ! ;
hence card { F where F is Function of X,X : F is Permutation of X } = (card X) ! by A5, Th7; :: thesis: verum