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:51;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A2, LAPLACE:11, NAT_D:26; :: thesis: verum

end;

suppose A3: 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 A3, NAT_1:21;
reconsider R = r as Element of Permutations (n2 + 2) ;
set K = the Fanoian Field;
set S = 2Set (Seg (n2 + 2));
2Set (Seg (n2 + 2)) in Fin (2Set (Seg (n2 + 2))) by FINSUB_1:def 5;
then A4: In ((2Set (Seg (n2 + 2))),(Fin (2Set (Seg (n2 + 2))))) = 2Set (Seg (n2 + 2)) by SUBSET_1:def 8;
idseq (n2 + 2) is Element of (Group_of_Perm (n2 + 2)) by MATRIX_1:11;
then reconsider I = idseq (n2 + 2) as Element of Permutations (n2 + 2) by MATRIX_1:def 13;
set D = { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn (I, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . s ) } ;
A5: { s where s is Element of 2Set (Seg (n2 + 2)) : ( s in 2Set (Seg (n2 + 2)) & (Part_sgn (I, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . s ) } c= 2Set (Seg (n2 + 2))

proof

let x be object ; :: 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, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . 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, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . 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, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . 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, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . s ) } as finite set ;
2Set (Seg (n2 + 2)) c= D

proof

let x be object ; :: 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
A6: i in Seg (n2 + 2) and
A7: j in Seg (n2 + 2) and
A8: i < j and
A9: s = {i,j} by MATRIX11:1;
A10: I . j = j by A7, FUNCT_1:17;
reconsider i9 = i, j9 = j, n29 = n2 as Element of NAT by ORDINAL1:def 12;
A11: j9 <= n2 + 2 by A7, FINSEQ_1:1;
i9 <= n29 + 2 by A6, FINSEQ_1:1;
then reconsider ni = ((n29 + 2) - i9) + 1, nj = ((n29 + 2) - j9) + 1 as Element of NAT by A11, FINSEQ_5:1;
ni in Seg (n2 + 2) by A6, FINSEQ_5:2;
then A12: I . ni = ni by FUNCT_1:17;
A13: len (idseq (n2 + 2)) = n29 + 2 by CARD_1:def 7;
i in dom I by A6;
then A14: R . i9 = I . ni by A1, A13, FINSEQ_5:58;
j in dom I by A7;
then A15: R . j9 = I . nj by A1, A13, FINSEQ_5:58;
nj in Seg (n2 + 2) by A7, FINSEQ_5:2;
then A16: I . nj = nj by FUNCT_1:17;
I . i = i by A6, FUNCT_1:17;
then A17: (Part_sgn (I, the Fanoian Field)) . s = 1_ the Fanoian Field by A6, A7, A8, A9, A10, MATRIX11:def 1;
((n29 + 2) + 1) - i9 > ((n29 + 2) + 1) - j9 by A8, XREAL_1:15;
then (Part_sgn (R, the Fanoian Field)) . s = - (1_ the Fanoian Field) by A6, A7, A8, A9, A14, A15, A12, A16, MATRIX11:def 1;
then (Part_sgn (I, the Fanoian Field)) . s <> (Part_sgn (R, the Fanoian Field)) . s by A17, MATRIX11:22;
hence x in D ; :: thesis: verum

end;

then A18: 2Set (Seg (n2 + 2)) = D by A5, XBOOLE_0:def 10;
A19: 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 A20: (n choose 2) mod 2 = 0 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

A21: sgn (I, the Fanoian Field) = 1_ the Fanoian Field by MATRIX11:12;
sgn (I, the Fanoian Field) = sgn (R, the Fanoian Field) by A18, A4, A19, A20, MATRIX11:7;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A20, A21, MATRIX11:23; :: thesis: verum

end;

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

A23: sgn (I, the Fanoian Field) = 1_ the Fanoian Field by MATRIX11:12;
sgn (R, the Fanoian Field) = - (sgn (I, the Fanoian Field)) by A18, A4, A19, A22, MATRIX11:7;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A22, A23, MATRIX11:23; :: thesis: verum

end;

end;

end;

end;