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 ( not perm2 is even & K is Fanoian ) or ( perm2 is even & not K is Fanoian ) or ( not perm2 is even & 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_2:def 16;
sgn perm2,K = 1_ K by A1, Th23;
hence - a,perm2 = (sgn perm2,K) * a by A2, VECTSP_1:def 13; :: thesis: verum

end;

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

then A4: - a,perm2 = - a by MATRIX_2:def 16;
A5: (- (1_ K)) * a = - ((1_ K) * a) by VECTSP_1:40;
sgn perm2,K = - (1_ K) by A3, Th23;
hence - a,perm2 = (sgn perm2,K) * a by A4, A5, VECTSP_1:def 13; :: 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_2: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 13; :: thesis: verum

end;

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

then A10: - a,perm2 = - a by MATRIX_2:def 16;
A11: (- (1_ K)) * a = - ((1_ K) * a) by VECTSP_1:40;
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 13; :: thesis: verum

end;

end;