A1: Permutations n c= Funcs ((Seg n),(Seg n))

proof

let x be object ; :: 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 Def12;
hence x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9; :: thesis: verum

end;

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