let n be Nat; :: thesis: for K being commutative Ring
for p being Element of Permutations n
for x being Element of K st n >= 1 holds
- (x,p) = - (x,(p "))
let K be commutative Ring; :: 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_1:def 12;
A2: len (Permutations n) = n by MATRIX_1:9;

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

end;

end;