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

hence card (Permutations n) = (card (finSeg N)) ! by CARD_FIN:8

.= n ! by FINSEQ_1:57 ;

:: thesis: verum

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

{ F where F is Function of (finSeg N),(finSeg N) : F is Permutation of (finSeg N) } c= Permutations n
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;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

proof

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;
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;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

hence card (Permutations n) = (card (finSeg N)) ! by CARD_FIN:8

.= n ! by FINSEQ_1:57 ;

:: thesis: verum