let p be Permutation of (Seg 3); :: thesis: ( p = <*2,3,1*> implies not p is being_transposition )
assume A1: p = <*2,3,1*> ; :: thesis: not p is being_transposition
then A2: dom p = {1,2,3} by ;
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 ;
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 ;
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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ; :: 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 ;
end;
end;
hence not p is being_transposition by MATRIX_1:def 14; :: thesis: verum