theorem Th11: :: MATRIX_7:11

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