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 9;
A2: len (Permutations n) = n by MATRIX_2:18;

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 13;
hence - (x,p) = - (x,(p ")) by A2, MATRIX_2:def 13; :: 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 13;
hence - (x,p) = - (x,(p ")) by MATRIX_2:def 13; :: thesis: verum

end;

end;