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 " )
A2: len (Permutations n) = n by MATRIX_2:20;
reconsider pf = p as Permutation of (Seg n) by MATRIX_2:def 11;

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

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

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

end;

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

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

end;

end;