defpred S_{1}[ object ] means $1 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();

take P ; :: thesis: for x being set holds

( x in P iff x is Permutation of (Seg n) )

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

consider P being set such that

A1: for x being object holds

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

take P ; :: thesis: for x being set holds

( x in P iff x is Permutation of (Seg n) )

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