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 ) )

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

hence
not p is being_transposition
by MATRIX_1:def 14; :: thesis: verum
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 )

A13: ( k <> i & k <> j ) and

A14: k in dom p ;

A15: p . k = k by A5, A13, A14;

end;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

then consider k being Nat such that
A6:
( i = 1 or i = 2 or i = 3 )
by A2, A3, ENUMSET1:def 1;

end;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;

end;

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

( k <> i & k <> j & k in dom p )

( 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;thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A7, ENUMSET1:def 1; :: thesis: verum

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

( k <> i & k <> j & k in dom p )

( 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;thus ( 1 <> i & 1 <> j & 1 in dom p ) by A2, A8, ENUMSET1:def 1; :: thesis: verum

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

( k <> i & k <> j & k in dom p )

( 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;thus ( 2 <> i & 2 <> j & 2 in dom p ) by A2, A9, ENUMSET1:def 1; :: thesis: verum

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

( k <> i & k <> j & k in dom p )

( 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;thus ( 3 <> i & 3 <> j & 3 in dom p ) by A2, A10, ENUMSET1:def 1; :: thesis: verum

A13: ( k <> i & k <> j ) and

A14: k in dom p ;

A15: p . k = k by A5, A13, A14;