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

now

assume A2: p = <*1,2*> ; :: thesis: contradiction
set p0 = <*1,2*>;
A3: len <*1,2*> = 2 by FINSEQ_1:61;
consider i, j being Nat such that
A4: ( 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 ) ) by A1, MATRIX_2:def 14;
A5: dom p = {1,2} by A2, A3, FINSEQ_1:4, FINSEQ_1:def 3;
then A6: ( i = 1 or i = 2 ) by A4, TARSKI:def 2;

now

per cases ( ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) ) by A4, A5, A6, TARSKI:def 2;

case ( i = 1 & j = 2 ) ; :: thesis: contradiction

hence contradiction by A2, A4, FINSEQ_1:61; :: thesis: verum

end;

case ( i = 2 & j = 1 ) ; :: thesis: contradiction

hence contradiction by A2, A4, FINSEQ_1:61; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

hence p = <*2,1*> by Th1; :: thesis: verum