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, FINSEQ_1:44; :: thesis: verum
end;
case ( i = 2 & j = 1 ) ; :: thesis: contradiction
hence contradiction by A2, A5, FINSEQ_1:44; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence p = <*2,1*> by Th1; :: thesis: verum