let l be FinSequence of (Group_of_Perm 3); :: thesis: ( (len l) mod 2 = 0 & ( for i being 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*> implies Product l = <*3,1,2*> )

assume that

A1: (len l) mod 2 = 0 and

A2: for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> )

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 ) by A2;

hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by A1, Th41; :: thesis: verum

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*> implies Product l = <*3,1,2*> )

assume that

A1: (len l) mod 2 = 0 and

A2: for i being Nat st i in dom l holds

ex q being Element of Permutations 3 st

( l . i = q & q is being_transposition ) ; :: thesis: ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> )

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 ) by A2;

hence ( Product l = <*1,2,3*> or Product l = <*2,3,1*> or Product l = <*3,1,2*> ) by A1, Th41; :: thesis: verum