:: deftheorem Def2 defines eval POLYNOM4:def 2 :
for L being non empty unital doubleLoopStr
for p being Polynomial of L
for x, b₄ being Element of L holds
( b₄ = eval (p,x) iff ex F being FinSequence of the carrier of L st
( b₄ = Sum F & len F = len p & ( for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * ((power L) . (x,(n -' 1))) ) ) );