let n be Nat; :: thesis: for perm2 being Element of Permutations (n + 2)
for K being Fanoian Field holds
( ( perm2 is even implies sgn perm2,K = 1_ K ) & ( sgn perm2,K = 1_ K implies perm2 is even ) & ( not perm2 is even implies sgn perm2,K = - (1_ K) ) & ( sgn perm2,K = - (1_ K) implies not perm2 is even ) )
let perm2 be Element of Permutations (n + 2); :: thesis: for K being Fanoian Field holds
( ( perm2 is even implies sgn perm2,K = 1_ K ) & ( sgn perm2,K = 1_ K implies perm2 is even ) & ( not perm2 is even implies sgn perm2,K = - (1_ K) ) & ( sgn perm2,K = - (1_ K) implies not perm2 is even ) )
set n2 = n + 2;
let K be Fanoian Field; :: thesis: ( ( perm2 is even implies sgn perm2,K = 1_ K ) & ( sgn perm2,K = 1_ K implies perm2 is even ) & ( not perm2 is even implies sgn perm2,K = - (1_ K) ) & ( sgn perm2,K = - (1_ K) implies not perm2 is even ) )
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_2:20;
thus A2: ( perm2 is even implies sgn perm2,K = 1_ K ) :: thesis: ( ( sgn perm2,K = 1_ K implies perm2 is even ) & ( not perm2 is even implies sgn perm2,K = - (1_ K) ) & ( sgn perm2,K = - (1_ K) implies not perm2 is even ) )

proof

assume perm2 is even ; :: thesis: sgn perm2,K = 1_ K
then ex L being FinSequence of (Group_of_Perm (n + 2)) st
( (len L) mod 2 = 0 & perm2 = Product L & ( for i being Nat st i in dom L holds
ex q2 being Element of Permutations (n + 2) st
( L . i = q2 & q2 is being_transposition ) ) ) by A1, MATRIX_2:def 15;
hence sgn perm2,K = 1_ K by Th15; :: thesis: verum

end;

thus ( sgn perm2,K = 1_ K implies perm2 is even ) :: thesis: ( not perm2 is even iff sgn perm2,K = - (1_ K) )

proof

assume A3: sgn perm2,K = 1_ K ; :: thesis: perm2 is even
consider P being FinSequence of (Group_of_Perm (n + 2)) such that
A4: perm2 = Product P and
A5: for i being Nat st i in dom P holds
ex trans being Element of Permutations (n + 2) st
( P . i = trans & trans is being_transposition ) by Th21;
assume not perm2 is even ; :: thesis: contradiction
then (len P) mod 2 <> 0 by A1, A4, A5, MATRIX_2:def 15;
then (len P) mod 2 = 1 by NAT_D:12;
then sgn perm2,K = - (1_ K) by A4, A5, Th15;
hence contradiction by A3, Th22; :: thesis: verum

end;

hence ( not perm2 is even iff sgn perm2,K = - (1_ K) ) by A2, Th11, Th22; :: thesis: verum