for n being Nat
for p1 being Element of Permutations (n + 1)
for K being Field
for a being Element of K
for i, j being Nat st i in Seg (n + 1) & p1 . i = j holds
- (a,p1) = ((power K) . ((- (1_ K)),(i + j))) * (- (a,(Rem (p1,i))))