let n be Nat; :: thesis: for K being commutative Ring
for a being Element of K
for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a
let K be commutative Ring; :: thesis: for a being Element of K
for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a
let a be Element of K; :: thesis: for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a
let perm2 be Element of Permutations (n + 2); :: thesis: - (a,perm2) = (sgn (perm2,K)) * a
A1: len (Permutations (n + 2)) = n + 2 by MATRIX_1:9;

per cases ( perm2 is even or perm2 is odd ) ;

suppose A2: perm2 is even ; :: thesis: - (a,perm2) = (sgn (perm2,K)) * a

then sgn (perm2,K) = 1_ K by A1, Th15;
hence (sgn (perm2,K)) * a = a
.= - (a,perm2) by A2, MATRIX_1:def 16 ;
:: thesis: verum

end;

suppose A10: perm2 is odd ; :: thesis: - (a,perm2) = (sgn (perm2,K)) * a

consider P being FinSequence of (Group_of_Perm (n + 2)) such that
A11: ( perm2 = Product P & ( 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;
for l being FinSequence of (Group_of_Perm (n + 2)) st perm2 = Product l & ( for i being Nat st i in dom l holds
ex q being Element of Permutations (n + 2) st
( l . i = q & q is being_transposition ) ) holds
(len l) mod 2 = 1 by A1, A10, NAT_D:12;
then A13: (len P) mod 2 = 1 by A11;
A14: - (a,perm2) = - a by A10, MATRIX_1:def 16;
sgn (perm2,K) = - (1_ K) by A13, A11, Th15;
hence (sgn (perm2,K)) * a = (- (1_ K)) * a
.= - a by VECTSP_2:29
.= - (a,perm2) by A14 ;
:: thesis: verum

end;

end;