let a, b be Element of (Group_of_Perm 2); :: thesis: ( ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) implies a * b = <*1,2*> )
assume A1: ( ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) & ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) ) ; :: thesis: a * b = <*1,2*>
then A2: a = <*2,1*> by Th8;
A3: b = <*2,1*> by A1, Th8;
the carrier of (Group_of_Perm 2) = Permutations 2 by MATRIX_2:def 13;
then A4: ( a * b = <*1,2*> or a * b = <*2,1*> ) by Th3, TARSKI:def 2;
consider p being Element of Permutations 2 such that
A5: ( p = a & p is being_transposition ) by A1;
consider q being Element of Permutations 2 such that
A6: ( q = b & q is being_transposition ) by A1;
A7: a * b = q * p by A5, A6, MATRIX_2:def 13;
reconsider q2 = q as FinSequence by A6, Th8;
A8: ( len q2 = 2 & q2 . 1 = 2 & q2 . 2 = 1 ) by A3, A6, FINSEQ_1:61;
reconsider p2 = p as FinSequence by A5, Th8;
A9: ( len p2 = 2 & p2 . 1 = 2 & p2 . 2 = 1 ) by A2, A5, FINSEQ_1:61;
then 1 in Seg (len p2) ;
then 1 in dom p2 by FINSEQ_1:def 3;
then (q * p) . 1 = 1 by A8, A9, FUNCT_1:23;
hence a * b = <*1,2*> by A4, A7, FINSEQ_1:61; :: thesis: verum