let p be Permutation of (Seg 3); :: thesis: ( p = <*3,2,1*> implies p is being_transposition )

assume A1: p = <*3,2,1*> ; :: thesis: p is being_transposition

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

assume A1: p = <*3,2,1*> ; :: thesis: p is being_transposition

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

proof

hence
p is being_transposition
by MATRIX_1:def 14; :: thesis: verum
take i = 1; :: thesis: ex 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 j = 3; :: thesis: ( 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 ) )

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

for k being Nat st k <> i & k <> j & k in dom p holds

p . k = k

p . k = k ) ) by A1, FINSEQ_1:45; :: thesis: verum

end;( 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 j = 3; :: thesis: ( 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 ) )

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

for k being Nat st k <> i & k <> j & k in dom p holds

p . k = k

proof

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

assume ( k <> i & k <> j & k in dom p ) ; :: thesis: p . k = k

then k = 2 by A2, ENUMSET1:def 1;

hence p . k = k by A1, FINSEQ_1:45; :: thesis: verum

end;assume ( k <> i & k <> j & k in dom p ) ; :: thesis: p . k = k

then k = 2 by A2, ENUMSET1:def 1;

hence p . k = k by A1, FINSEQ_1:45; :: thesis: verum

p . k = k ) ) by A1, FINSEQ_1:45; :: thesis: verum