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

for l being FinSequence of (Group_of_Perm 2) holds

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

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

( not l . i = q or not q is being_transposition ) ) ) ) by Lm1, MATRIX_7:11;

then g is odd by MATRIX_1:def 15;

hence ex b_{1} being Permutation of (Seg 2) st b_{1} is odd
; :: thesis: verum

for l being FinSequence of (Group_of_Perm 2) holds

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

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

( not l . i = q or not q is being_transposition ) ) ) ) by Lm1, MATRIX_7:11;

then g is odd by MATRIX_1:def 15;

hence ex b