theorem Th24: :: POLYNOM4:24

for L being non trivial right_complementable Abelian add-associative right_zeroed distributive left_unital associative commutative doubleLoopStr
for p, q being Polynomial of L
for x being Element of L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))