theorem Th30: :: POLYNOM5:30

for L being non empty right_complementable almost_left_invertible add-associative right_zeroed well-unital distributive associative commutative doubleLoopStr
for p being Polynomial of L
for v, x being Element of L holds eval ((v * p),x) = v * (eval (p,x))