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 ( perm2 is even & K is Fanoian ) ; :: thesis: - a,perm2 = (sgn perm2,K) * a

then ( - a,perm2 = a & sgn perm2,K = 1_ K ) by Th23, MATRIX_2:def 16;
hence - a,perm2 = (sgn perm2,K) * a by VECTSP_1:def 13; :: thesis: verum

end;

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

then ( - a,perm2 = - a & sgn perm2,K = - (1_ K) & (- (1_ K)) * a = - ((1_ K) * a) ) by Th23, MATRIX_2:def 16, VECTSP_1:40;
hence - a,perm2 = (sgn perm2,K) * a by VECTSP_1:def 13; :: thesis: verum

end;

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

then ( - a,perm2 = a & 1_ K = - (1_ K) & ( sgn perm2,K = 1_ K or sgn perm2,K = - (1_ K) ) ) by Th11, Th22, MATRIX_2:def 16;
hence - a,perm2 = (sgn perm2,K) * a by VECTSP_1:def 13; :: thesis: verum

end;

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

then ( - a,perm2 = - a & 1_ K = - (1_ K) & (- (1_ K)) * a = - ((1_ K) * a) & ( sgn perm2,K = 1_ K or sgn perm2,K = - (1_ K) ) ) by Th11, Th22, MATRIX_2:def 16, VECTSP_1:40;
hence - a,perm2 = (sgn perm2,K) * a by VECTSP_1:def 13; :: thesis: verum

end;

end;