theorem :: POLYNOM7:30

for n being Ordinal
for L being non trivial left_add-cancelable right_complementable add-associative right_zeroed well-unital distributive associative 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 ((a * p),x) = a * (eval (p,x))