let P1, P2 be set ; :: thesis: ( ( for x being set holds
( x in P1 iff x is Permutation of (Seg n) ) ) & ( for x being set holds
( x in P2 iff x is Permutation of (Seg n) ) ) implies P1 = P2 )
assume that
A3: for x being set holds
( x in P1 iff x is Permutation of (Seg n) ) and
A4: for x being set holds
( x in P2 iff x is Permutation of (Seg n) ) ; :: thesis: P1 = P2

A5: now :: thesis: for x being object st x in P2 holds
x in P1

let x be object ; :: thesis: ( x in P2 implies x in P1 )
assume x in P2 ; :: thesis: x in P1
then x is Permutation of (Seg n) by A4;
hence x in P1 by A3; :: thesis: verum

end;

now :: thesis: for x being object st x in P1 holds
x in P2

let x be object ; :: thesis: ( x in P1 implies x in P2 )
assume x in P1 ; :: thesis: x in P2
then x is Permutation of (Seg n) by A3;
hence x in P2 by A4; :: thesis: verum

end;

hence P1 = P2 by A5, TARSKI:2; :: thesis: verum