let n be Nat; :: thesis: Permutations n is finite
A1: Permutations n c= Funcs ((Seg n),(Seg n))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Permutations n or x in Funcs ((Seg n),(Seg n)) )
assume x in Permutations n ; :: thesis: x in Funcs ((Seg n),(Seg n))
then x is Function of (Seg n),(Seg n) by Def11;
hence x in Funcs ((Seg n),(Seg n)) by FUNCT_2:12; :: thesis: verum

end;

Funcs ((Seg n),(Seg n)) is finite by FRAENKEL:16;
hence Permutations n is finite by A1, FINSET_1:13; :: thesis: verum