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 that
A1: ex p being Element of Permutations 2 st
( p = a & p is being_transposition ) and
A2: ex q being Element of Permutations 2 st
( q = b & q is being_transposition ) ; :: thesis: a * b = <*1,2*>
consider p being Element of Permutations 2 such that
A3: p = a and
A4: p is being_transposition by A1;
the carrier of (Group_of_Perm 2) = Permutations 2 by MATRIX_1:def 13;
then A5: ( a * b = <*1,2*> or a * b = <*2,1*> ) by Th3, TARSKI:def 2;
reconsider p2 = p as FinSequence by A3, A4, Th8;
A6: a = <*2,1*> by A1, Th8;
then len p2 = 2 by A3, FINSEQ_1:44;
then 1 in Seg (len p2) ;
then A7: 1 in dom p2 by FINSEQ_1:def 3;
consider q being Element of Permutations 2 such that
A8: q = b and
A9: q is being_transposition by A2;
reconsider q2 = q as FinSequence by A8, A9, Th8;
b = <*2,1*> by A2, Th8;
then A10: q2 . 2 = 1 by A8, FINSEQ_1:44;
A11: a * b = q * p by A3, A8, MATRIX_1:def 13;
p2 . 1 = 2 by A6, A3, FINSEQ_1:44;
then (q * p) . 1 = 1 by A10, A7, FUNCT_1:13;
hence a * b = <*1,2*> by A5, A11, FINSEQ_1:44; :: thesis: verum