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