:: deftheorem Def13 defines Polynomial-Function POLYNOM5:def 13 :
for L being non empty well-unital doubleLoopStr
for p being Polynomial of L
for b₃ being Function of L,L holds
( b₃ = Polynomial-Function (L,p) iff for x being Element of L holds b₃ . x = eval (p,x) );