:: deftheorem Def10 defines Jpolynom POLYNOM9:def 10 :
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for m being Nat st m > 1 holds
for b₃ being Polynomial of m,L holds
( b₃ is Jpolynom of m,L iff ( b₃ . ((EmptyBag m) +* (0,(2 |^ (m -' 1)))) = 1. L & ( for b being bag of m st b in Support b₃ holds
( degree b = 2 |^ (m -' 1) & ex i being Integer st b₃ . b = i '*' (1_ L) & ( not 2 |^ (m -' 1) in rng b or b₃ . b = 1. L or b₃ . b = - (1. L) ) & ( for n being Nat holds b . n is even ) ) ) & ( for f being FinSequence of L
for xf being Function of m,L st xf = FS2XFS f holds
eval (b₃,xf) = SignGenOp (f, the multF of L, the addF of L,((Seg m) \ {1})) ) ) );