let n be Nat; :: thesis: for K being commutative Ring
for perm2 being Element of Permutations (n + 2) st K is Fanoian & not K is degenerated holds
( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
let K be commutative Ring; :: thesis: for perm2 being Element of Permutations (n + 2) st K is Fanoian & not K is degenerated holds
( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
let perm2 be Element of Permutations (n + 2); :: thesis: ( K is Fanoian & not K is degenerated implies ( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) ) )
assume A0: ( K is Fanoian & not K is degenerated ) ; :: thesis: ( ( perm2 is even implies sgn (perm2,K) = 1_ K ) & ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
set n2 = n + 2;
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_1:9;
thus A2: ( perm2 is even implies sgn (perm2,K) = 1_ K ) by A1, Th15; :: thesis: ( ( sgn (perm2,K) = 1_ K implies perm2 is even ) & ( perm2 is odd implies sgn (perm2,K) = - (1_ K) ) & ( sgn (perm2,K) = - (1_ K) implies perm2 is odd ) )
thus ( sgn (perm2,K) = 1_ K implies perm2 is even ) :: thesis: ( perm2 is odd 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 perm2 is odd ; :: thesis: contradiction
then (len P) mod 2 <> 0 by A1, A4, A5;
then (len P) mod 2 = 1 by NAT_D:12;
then sgn (perm2,K) = - (1_ K) by A4, A5, Th15;
hence contradiction by A0, A3, th22; :: thesis: verum

end;

hence ( perm2 is odd iff sgn (perm2,K) = - (1_ K) ) by A0, A2, Th11, th22; :: thesis: verum