let n be Nat; :: thesis: for R being Element of Permutations n st R = Rev (idseq n) holds
( R is even iff (n choose 2) mod 2 = 0 )
let r be Element of Permutations n; :: thesis: ( r = Rev (idseq n) implies ( r is even iff (n choose 2) mod 2 = 0 ) )
assume A1: r = Rev (idseq n) ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

per cases ( n < 2 or n >= 2 ) ;

suppose A2: n < 2 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

then ( n = 0 or n = 1 ) by NAT_1:23;
then (n * (n - 1)) / 2 = 0 ;
then n choose 2 = 0 by STIRL2_1:61;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A2, LAPLACE:11, NAT_D:26; :: thesis: verum

end;

suppose A4: n >= 2 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

set CH = n choose 2;
reconsider n2 = n - 2 as Nat by A4, NAT_1:21;
reconsider R = r as Element of Permutations (n2 + 2) ;
consider K being Fanoian Field;
set S = 2Set (Seg (n2 + 2));
A5: FinOmega (2Set (Seg (n2 + 2))) = 2Set (Seg (n2 + 2)) by MATRIX_2:def 17;
idseq (n2 + 2) is Element of (Group_of_Perm (n2 + 2)) by MATRIX_2:23;
then reconsider I = idseq (n2 + 2) as Element of Permutations (n2 + 2) by MATRIX_2:def 13;
set D = { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) } ;
A6: { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) } c= 2Set (Seg (n2 + 2))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) } or x in 2Set (Seg (n2 + 2)) )
assume x in { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) } ; :: thesis: x in 2Set (Seg (n2 + 2))
then ex s being Element of 2Set (Seg (n2 + 2)) st
( x = s & s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) ;
hence x in 2Set (Seg (n2 + 2)) ; :: thesis: verum

end;

then reconsider D = { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn I,K) . s <> (Part_sgn R,K) . s ) } as finite set ;
2Set (Seg (n2 + 2)) c= D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in 2Set (Seg (n2 + 2)) or x in D )
assume x in 2Set (Seg (n2 + 2)) ; :: thesis: x in D
then reconsider s = x as Element of 2Set (Seg (n2 + 2)) ;
consider i, j being Nat such that
A7: i in Seg (n2 + 2) and
A8: j in Seg (n2 + 2) and
A9: i < j and
A10: s = {i,j} by MATRIX11:1;
A11: I . j = j by A8, FUNCT_1:34;
reconsider i9 = i, j9 = j, n29 = n2 as Element of NAT by ORDINAL1:def 13;
A12: j9 <= n2 + 2 by A8, FINSEQ_1:3;
i9 <= n29 + 2 by A7, FINSEQ_1:3;
then reconsider ni = ((n29 + 2) - i9) + 1, nj = ((n29 + 2) - j9) + 1 as Element of NAT by A12, FINSEQ_5:1;
ni in Seg (n2 + 2) by A7, FINSEQ_5:2;
then A13: I . ni = ni by FUNCT_1:34;
A14: len (idseq (n2 + 2)) = n29 + 2 by FINSEQ_1:def 18;
then i in dom I by A7, FINSEQ_1:def 3;
then A15: R . i9 = I . ni by A1, A14, FINSEQ_5:61;
j in dom I by A8, A14, FINSEQ_1:def 3;
then A16: R . j9 = I . nj by A1, A14, FINSEQ_5:61;
nj in Seg (n2 + 2) by A8, FINSEQ_5:2;
then A17: I . nj = nj by FUNCT_1:34;
I . i = i by A7, FUNCT_1:34;
then A18: (Part_sgn I,K) . s = 1_ K by A7, A8, A9, A10, A11, MATRIX11:def 1;
((n29 + 2) + 1) - i9 > ((n29 + 2) + 1) - j9 by A9, XREAL_1:17;
then (Part_sgn R,K) . s = - (1_ K) by A7, A8, A9, A10, A15, A16, A13, A17, MATRIX11:def 1;
then (Part_sgn I,K) . s <> (Part_sgn R,K) . s by A18, MATRIX11:22;
hence x in D ; :: thesis: verum

end;

then A19: 2Set (Seg (n2 + 2)) = D by A6, XBOOLE_0:def 10;
A20: card (2Set (Seg (n2 + 2))) = n choose 2 by Th10;

per cases ( (n choose 2) mod 2 = 0 or (n choose 2) mod 2 = 1 ) by NAT_D:12;

suppose A21: (n choose 2) mod 2 = 0 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

A22: sgn I,K = 1_ K by MATRIX11:12;
sgn I,K = sgn R,K by A19, A5, A20, A21, MATRIX11:7;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A21, A22, MATRIX11:23; :: thesis: verum

end;

suppose A23: (n choose 2) mod 2 = 1 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

A24: sgn I,K = 1_ K by MATRIX11:12;
sgn R,K = - (sgn I,K) by A19, A5, A20, A23, MATRIX11:7;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A23, A24, MATRIX11:23; :: thesis: verum

end;

end;

end;

end;