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