theorem Th59:
for
L being non
empty non
trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr for
n being
Nat for
f being
FinSequence of
L for
xf being
Function of
n,
L st
xf = FS2XFS f holds
for
F being
finite set for
E being
Enumeration of
F for
d being
FinSequence st
d in doms ((SignGenOp (f, the addF of L,F)) * E) holds
the
multF of
L "**" ((App ((SignGenOp (f, the addF of L,F)) * E)) . d) = eval (
(Monom ((SgnMembershipNumber (d,L,E)),(count_reps (d,n)))),
xf)