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 :: thesis: not p = <*1,2*>

set p0 = <*1,2*>;
assume A2: p = <*1,2*> ; :: thesis: contradiction
consider i, j being Nat such that
A3: i in dom p and
A4: ( j in dom p & i <> j ) and
A5: p . i = j and
p . j = i and
for k being Nat st k <> i & k <> j & k in dom p holds
p . k = k by A1;
len <*1,2*> = 2 by FINSEQ_1:44;
then A6: dom p = {1,2} by A2, FINSEQ_1:2, FINSEQ_1:def 3;
then A7: ( i = 1 or i = 2 ) by A3, TARSKI:def 2;

now :: thesis: ( ( i = 1 & j = 2 & contradiction ) or ( i = 2 & j = 1 & contradiction ) )

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

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

hence contradiction by A2, A5; :: thesis: verum

end;

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

hence contradiction by A2, A5; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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