:: deftheorem Def3 defines Polynom-Evaluation POLYNOM2:def 5 :
for n being Ordinal
for L being non trivial right_complementable add-associative right_zeroed well-unital distributive doubleLoopStr
for x being Function of n,L
for b₄ being Function of (Polynom-Ring (n,L)),L holds
( b₄ = Polynom-Evaluation (n,L,x) iff for p being Polynomial of n,L holds b₄ . p = eval (p,x) );