for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative commutative domRing-like left_zeroed doubleLoopStr
for p being Polynomial of n,L
for a being Element of L
for x being Function of n,L holds eval ((p * a),x) = (eval (p,x)) * a