let n be 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
let K be 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
let a be 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
let perm2 be Element of Permutations (n + 2); ( not K is degenerated & K is well-unital & K is domRing-like implies - (a,perm2) = (sgn (perm2,K)) * a )
assume A0:
( not K is degenerated & K is well-unital & K is domRing-like )
; - (a,perm2) = (sgn (perm2,K)) * a