reconsider f = <*3,2,1*> 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 Lm3, Lm7, Lm17;
then f is odd by MATRIX_1:def 15;
hence ex b₁ being Permutation of (Seg 3) st b₁ is odd ; :: thesis: verum