let n be Nat; :: thesis: card (Permutations n) = n !
set P = Permutations n;
reconsider N = n as Element of NAT by ORDINAL1:def 12;
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 object ; :: 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_1:def 12;
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 object ; :: 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_1:def 12; :: 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:57 ;
:: thesis: verum