defpred S₁[ set ] means n is Permutation of (Seg n);
consider P being set such that
A1: for x being set holds
( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S₁[x] ) ) from XBOOLE_0:sch 1();
idseq n in Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
then reconsider P = P as non empty set by A1;

now

take n = n; :: thesis: for x being set st x in P holds
x is Permutation of (Seg n)
let x be set ; :: thesis: ( x in P implies x is Permutation of (Seg n) )
assume x in P ; :: thesis: x is Permutation of (Seg n)
hence x is Permutation of (Seg n) by A1; :: thesis: verum

end;

then reconsider P = P as non empty permutational set by Def9;
for x being set holds
( x in P iff x is Permutation of (Seg n) )

proof

let x be set ; :: thesis: ( x in P iff x is Permutation of (Seg n) )
thus ( x in P implies x is Permutation of (Seg n) ) by A1; :: thesis: ( x is Permutation of (Seg n) implies x in P )
assume A2: x is Permutation of (Seg n) ; :: thesis: x in P
then x in Funcs ((Seg n),(Seg n)) by FUNCT_2:9;
hence x in P by A1, A2; :: thesis: verum

end;

hence ( Permutations n is permutational & not Permutations n is empty ) by Def11; :: thesis: verum