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

proof

given i, j being Nat such that A3: i in dom p and
A4: ( j in dom p & i <> j ) and
p . i = j and
p . j = i and
A5: for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k ; :: thesis: contradiction
ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

proof

A6: ( i = 1 or i = 2 or i = 3 ) by A2, A3, ENUMSET1:def 1;

per cases ( ( i = 1 & j = 2 ) or ( i = 2 & j = 3 ) or ( i = 1 & j = 3 ) or ( i = 2 & j = 1 ) or ( i = 3 & j = 1 ) or ( i = 3 & j = 2 ) ) by A2, A4, A6, ENUMSET1:def 1;

suppose A7: ( i = 1 & j = 2 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 3 ; :: thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A7, ENUMSET1:def 1; :: thesis: verum

end;

suppose A8: ( i = 2 & j = 3 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 1 ; :: thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A8, ENUMSET1:def 1; :: thesis: verum

end;

suppose A9: ( i = 1 & j = 3 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 2 ; :: thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A9, ENUMSET1:def 1; :: thesis: verum

end;

suppose A10: ( i = 2 & j = 1 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 3 ; :: thesis: ( 3 <> i & 3 <> j & 3 in dom p )
thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A10, ENUMSET1:def 1; :: thesis: verum

end;

suppose A11: ( i = 3 & j = 1 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 2 ; :: thesis: ( 2 <> i & 2 <> j & 2 in dom p )
thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A11, ENUMSET1:def 1; :: thesis: verum

end;

suppose A12: ( i = 3 & j = 2 ) ; :: thesis: ex k being Element of NAT st
( k <> i & k <> j & k in dom p )

take 1 ; :: thesis: ( 1 <> i & 1 <> j & 1 in dom p )
thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A12, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

then consider k being Nat such that
A13: ( k <> i & k <> j ) and
A14: k in dom p ;
A15: p . k = k by A5, A13, A14;

per cases ( k = 1 or k = 2 or k = 3 ) by A2, A14, ENUMSET1:def 1;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A1, A15; :: thesis: verum

end;

suppose k = 2 ; :: thesis: contradiction

hence contradiction by A1, A15; :: thesis: verum

end;

suppose k = 3 ; :: thesis: contradiction

hence contradiction by A1, A15; :: thesis: verum

end;

end;

end;

hence not p is being_transposition by MATRIX_1:def 14; :: thesis: verum