let n be Element of NAT ; :: thesis: for K being Field
for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- x,p = - x,(p " )
let K be Field; :: thesis: for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- x,p = - x,(p " )
let p be Element of Permutations n; :: thesis: for x being Element of K st n >= 1 holds
- x,p = - x,(p " )
let x be Element of K; :: thesis: ( n >= 1 implies - x,p = - x,(p " ) )
assume A1: n >= 1 ; :: thesis: - x,p = - x,(p " )
reconsider pf = p as Permutation of (Seg n) by MATRIX_2:def 11;
A2: len (Permutations n) = n by MATRIX_2:20;

per cases ( p is even or not p is even ) ;

suppose p is even ; :: thesis: - x,p = - x,(p " )

then ( - x,p = x & pf " is even ) by A1, A2, Th28, MATRIX_2:def 16;
hence - x,p = - x,(p " ) by A2, MATRIX_2:def 16; :: thesis: verum

end;

suppose not p is even ; :: thesis: - x,p = - x,(p " )

then ( - x,p = - x & not p " is even ) by A1, Th28, MATRIX_2:def 16;
hence - x,p = - x,(p " ) by MATRIX_2:def 16; :: thesis: verum

end;

end;