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 & n in NAT ) ;
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 n >= 2 ; :: thesis: ( r is even iff (n choose 2) mod 2 = 0 )

then reconsider n2 = n - 2 as Nat by NAT_1:21;
reconsider R = r as Element of Permutations (n2 + 2) ;
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;
consider K being Fanoian Field;
set S = 2Set (Seg (n2 + 2));
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 ) } ;
A3: { 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
A4: ( i in Seg (n2 + 2) & j in Seg (n2 + 2) & i < j & s = {i,j} ) by MATRIX11:1;
reconsider i' = i, j' = j, n2' = n2 as Element of NAT by ORDINAL1:def 13;
( I . i = i & I . j = j ) by A4, FUNCT_1:34;
then A5: (Part_sgn I,K) . s = 1_ K by A4, MATRIX11:def 1;
A6: len (idseq (n2 + 2)) = n2' + 2 by FINSEQ_1:def 18;
( i' <= n2' + 2 & j' <= n2 + 2 ) by A4, FINSEQ_1:3;
then reconsider ni = ((n2' + 2) - i') + 1, nj = ((n2' + 2) - j') + 1 as Element of NAT by FINSEQ_5:1;
A7: ((n2' + 2) + 1) - i' > ((n2' + 2) + 1) - j' by A4, XREAL_1:17;
( i in dom I & j in dom I & ni in Seg (n2 + 2) & nj in Seg (n2 + 2) ) by A4, A6, FINSEQ_1:def 3, FINSEQ_5:2;
then ( R . i' = I . ni & R . j' = I . nj & I . ni = ni & I . nj = nj ) by A1, A6, FINSEQ_5:61, FUNCT_1:34;
then (Part_sgn R,K) . s = - (1_ K) by A4, A7, MATRIX11:def 1;
then (Part_sgn I,K) . s <> (Part_sgn R,K) . s by A5, MATRIX11:22;
hence x in D ; :: thesis: verum

end;

then A8: ( 2Set (Seg (n2 + 2)) = D & FinOmega (2Set (Seg (n2 + 2))) = 2Set (Seg (n2 + 2)) & card (2Set (Seg (n2 + 2))) = n choose 2 ) by A3, Th10, MATRIX_2:def 17, XBOOLE_0:def 10;
set CH = n choose 2;

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

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

then ( sgn I,K = sgn R,K & sgn I,K = 1_ K ) by A8, MATRIX11:7, MATRIX11:12;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A9, MATRIX11:23; :: thesis: verum

end;

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

then ( sgn R,K = - (sgn I,K) & sgn I,K = 1_ K ) by A8, MATRIX11:7, MATRIX11:12;
hence ( r is even iff (n choose 2) mod 2 = 0 ) by A10, MATRIX11:23; :: thesis: verum

end;

end;

end;

end;