let n be Nat; :: thesis: card () = 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 (),() : F is Permutation of () } ;
A1: Permutations n c= { F where F is Function of (),() : F is Permutation of () }
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 (),() : F is Permutation of () } )
assume x in Permutations n ; :: thesis: x in { F where F is Function of (),() : F is Permutation of () }
then x is Permutation of () by MATRIX_1:def 12;
hence x in { F where F is Function of (),() : F is Permutation of () } ; :: thesis: verum
end;
{ F where F is Function of (),() : F is Permutation of () } c= Permutations n
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { F where F is Function of (),() : F is Permutation of () } or x in Permutations n )
assume x in { F where F is Function of (),() : F is Permutation of () } ; :: thesis:
then ex F being Function of (),() st
( x = F & F is Permutation of () ) ;
hence x in Permutations n by MATRIX_1:def 12; :: thesis: verum
end;
then Permutations n = { F where F is Function of (),() : F is Permutation of () } by ;
hence card () = (card ()) ! by CARD_FIN:8
.= n ! by FINSEQ_1:57 ;
:: thesis: verum