theorem Th41: :: MATRIX_9:41

for l being FinSequence of (Group_of_Perm 3) st (len l) mod 2 = 0 & ( for i being Element of NAT st i in dom l holds
ex q being Element of Permutations 3 st
( l . i = q & q is being_transposition ) ) & not Product l = <*1,2,3*> & not Product l = <*2,3,1*> holds
Product l = <*3,1,2*>