let a be Element of (Group_of_Perm 2); :: thesis: ( ex q being Element of Permutations 2 st
( q = a & q is being_transposition ) implies a = <*2,1*> )
given q being Element of Permutations 2 such that A1: q = a and
A2: q is being_transposition ; :: thesis: a = <*2,1*>
the carrier of (Group_of_Perm 2) = Permutations 2 by MATRIX_1:def 13;
then reconsider b = a as Permutation of (Seg 2) by MATRIX_1:def 12;
ex i, j being Nat st
( i in dom q & j in dom q & i <> j & q . i = j & q . j = i & ( for k being Nat st k <> i & k <> j & k in dom q holds
q . k = k ) ) by A2;
then b is being_transposition by A1;
hence a = <*2,1*> by Th4; :: thesis: verum