:: deftheorem Def13 defines SignGenOp HILB10_7:def 13 :
for D being non empty set
for A, M being BinOp of D st M is commutative & M is associative holds
for f being FinSequence of D
for F being finite set
for b₆ being Element of D holds
( b₆ = SignGenOp (f,M,A,F) iff for E being Enumeration of bool F holds b₆ = M $$ (([#] (dom ((SignGenOp (f,A,(bool F))) * E))),(A "**" ((SignGenOp (f,A,(bool F))) * E))) );