defpred S₁[ 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₁[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