theorem Th17: :: POLYNOM2:25

for n being Ordinal
for L being non empty non trivial right_complementable associative commutative Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p, q being Polynomial of n,L
for x being Function of n,L holds eval ((p *' q),x) = (eval (p,x)) * (eval (q,x))