defpred S₁[ set ] means $1 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();
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:12;
hence x in P by A1, A2; :: thesis: verum