theorem Th23: :: POLYNOM4:23

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 (((Leading-Monomial p) *' q),x) = (eval ((Leading-Monomial p),x)) * (eval (q,x))