theorem Th26: :: MATRIX11:26

for n being Nat
for K being commutative Ring
for a being Element of K
for perm2 being Element of Permutations (n + 2) st not K is degenerated & K is well-unital & K is domRing-like holds
- (a,perm2) = (sgn (perm2,K)) * a