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 object ; :: 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 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 }
then consider F being Function of X,X such that
A2: x = F and
A3: F is one-to-one ;
card X = card X ;
then F is onto by A3, FINSEQ_4:63;
hence x in { F where F is Function of X,X : F is Permutation of X } by A2, A3; :: thesis: verum
end;
((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 }
proof
let x be object ; :: 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 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 }
then ex F being Function of X,X st
( x = F & F is Permutation of X ) ;
hence x in { F where F is Function of X,X : F is one-to-one } ; :: thesis: verum
end;
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; :: thesis: verum