defpred S_{1}[ 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_{1}[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;

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 Def5; :: thesis: verum

consider P being set such that

A1: for x being object holds

( x in P iff ( x in Funcs ((Seg n),(Seg n)) & S

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)

then reconsider P = P as non empty permutational set by Def3;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;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

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 Def5; :: thesis: verum