theorem Th30: :: RING_5:7

for R being domRing
for p being Polynomial of R
for v, x being Element of R holds eval ((v * p),x) = v * (eval (p,x))