let n be Nat; :: thesis: for K being Field
for a being Element of K
for perm2 being Element of Permutations (n + 2) holds - (a,perm2) = (sgn (perm2,K)) * a
let K be Field; :: 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

per cases ( ( perm2 is even & K is Fanoian ) or ( perm2 is odd & K is Fanoian ) or ( perm2 is even & not K is Fanoian ) or ( perm2 is odd & not K is Fanoian ) ) ;

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

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

end;

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

then A4: - (a,perm2) = - a by MATRIX_1:def 16;
A5: (- (1_ K)) * a = - ((1_ K) * a) by VECTSP_1:8;
sgn (perm2,K) = - (1_ K) by A3, Th23;
hence - (a,perm2) = (sgn (perm2,K)) * a by A4, A5, VECTSP_1:def 4; :: thesis: verum

end;

suppose A6: ( perm2 is even & not K is Fanoian ) ; :: thesis: - (a,perm2) = (sgn (perm2,K)) * a

then A7: - (a,perm2) = a by MATRIX_1:def 16;
A8: ( sgn (perm2,K) = 1_ K or sgn (perm2,K) = - (1_ K) ) by Th11;
1_ K = - (1_ K) by A6, Th22;
hence - (a,perm2) = (sgn (perm2,K)) * a by A7, A8, VECTSP_1:def 4; :: thesis: verum

end;

suppose A9: ( perm2 is odd & not K is Fanoian ) ; :: thesis: - (a,perm2) = (sgn (perm2,K)) * a

then A10: - (a,perm2) = - a by MATRIX_1:def 16;
A11: (- (1_ K)) * a = - ((1_ K) * a) by VECTSP_1:8;
A12: ( sgn (perm2,K) = 1_ K or sgn (perm2,K) = - (1_ K) ) by Th11;
1_ K = - (1_ K) by A9, Th22;
hence - (a,perm2) = (sgn (perm2,K)) * a by A10, A11, A12, VECTSP_1:def 4; :: thesis: verum

end;

end;