theorem Th15: :: POLYNOM2:23

for n being Ordinal
for L being non trivial right_complementable 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))