let p be Permutation of (Seg 3); :: thesis:
assume A1: p = <*1,3,2*> ; :: thesis:
then A2: dom p = {1,2,3} by FINSEQ_1:89, FINSEQ_3:1;
ex i, j being Nat st
( i in dom p & j in dom p & i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) )

take i = 2; :: thesis:
take j = 3; :: thesis:
thus ( i in dom p & j in dom p ) by A2, ENUMSET1:def 1; :: thesis:
for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k

let k be Nat; :: thesis:
assume ( k <> i & k <> j & k in dom p ) ; :: thesis:
then k = 1 by A2, ENUMSET1:def 1;
hence p . k = k by A1; :: thesis:

end;

hence ( i <> j & p . i = j & p . j = i & ( for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ) ) by A1; :: thesis:

end;