:: deftheorem Def3 defines Polynom-Evaluation POLYNOM4:def 3 :
for L being non empty right_complementable add-associative right_zeroed distributive unital doubleLoopStr
for x being Element of L
for b₃ being Function of (Polynom-Ring L),L holds
( b₃ = Polynom-Evaluation (L,x) iff for p being Polynomial of L holds b₃ . p = eval (p,x) );