reconsider f = <*1,3,2*> as Permutation of (Seg 3) by Th27, MATRIX_1:def 12;

for l being FinSequence of (Group_of_Perm 3) holds

( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st

( i in dom l & ( for q being Element of Permutations 3 holds

( not l . i = q or not q is being_transposition ) ) ) ) by Lm4, Lm9, Lm17;

hence <*1,3,2*> is odd Permutation of (Seg 3) by MATRIX_1:def 15; :: thesis: verum

for l being FinSequence of (Group_of_Perm 3) holds

( not (len l) mod 2 = 0 or not f = Product l or ex i being Nat st

( i in dom l & ( for q being Element of Permutations 3 holds

( not l . i = q or not q is being_transposition ) ) ) ) by Lm4, Lm9, Lm17;

hence <*1,3,2*> is odd Permutation of (Seg 3) by MATRIX_1:def 15; :: thesis: verum