:: deftheorem Def2 defines eval POLYNOM2:def 4 :
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of n,L
for x being Function of n,L
for b₅ being Element of L holds
( b₅ = eval (p,x) iff ex y being FinSequence of the carrier of L st
( len y = len (SgmX ((BagOrder n),(Support p))) & b₅ = Sum y & ( for i being Element of NAT st 1 <= i & i <= len y holds
y /. i = ((p * (SgmX ((BagOrder n),(Support p)))) /. i) * (eval (((SgmX ((BagOrder n),(Support p))) /. i),x)) ) ) );