defpred S₁[ object ] means n is Permutation of (Seg n);
consider P being set such that
A1: for x being object 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 :: thesis: ex n being Nat st
for x being set st x in P holds
x is Permutation of (Seg n)

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 Def10;
for x being set holds
( x in P iff x is Permutation of (Seg n) ) by A1, FUNCT_2:9;
hence ( Permutations n is permutational & not Permutations n is empty ) by Def12; :: thesis: verum