let n be Nat; :: thesis: card (Permutations n) = n !
set P = Permutations n;
reconsider N = n as Element of NAT by ORDINAL1:def 13;
set X = finSeg N;
set PER = { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } ;
A1: Permutations n c= { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } )
assume x in Permutations n ; :: thesis: x in { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N }
then x is Permutation of finSeg N by MATRIX_2:def 11;
hence x in { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } ; :: thesis: verum

end;

{ F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } c= Permutations n

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } or x in Permutations n )
assume x in { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } ; :: thesis: x in Permutations n
then ex F being Function of finSeg N, finSeg N st
( x = F & F is Permutation of finSeg N ) ;
hence x in Permutations n by MATRIX_2:def 11; :: thesis: verum

end;

then Permutations n = { F where F is Function of finSeg N, finSeg N : F is Permutation of finSeg N } by A1, XBOOLE_0:def 10;
hence card (Permutations n) = (card (finSeg N)) ! by CARD_FIN:8
.= n ! by FINSEQ_1:78 ;
:: thesis: verum