let a, b be Element of (Group_of_Perm 2); ( 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 )
; 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; verum