theorem Th7:
for
n being
Nat for
K being
commutative Ring for
X being
Element of
Fin (2Set (Seg (n + 2))) for
p2,
q2 being
Element of
Permutations (n + 2) for
F being
finite set st
F = { s where s is Element of 2Set (Seg (n + 2)) : ( s in X & (Part_sgn (p2,K)) . s <> (Part_sgn (q2,K)) . s ) } holds
( (
(card F) mod 2
= 0 implies the
multF of
K $$ (
X,
(Part_sgn (p2,K)))
= the
multF of
K $$ (
X,
(Part_sgn (q2,K))) ) & (
(card F) mod 2
= 1 implies the
multF of
K $$ (
X,
(Part_sgn (p2,K)))
= - ( the multF of K $$ (X,(Part_sgn (q2,K)))) ) )