theorem Th15: :: POLYNOM1:15

for n being set
for L being non empty addLoopStr
for p, q being Series of n,L
for x being bag of n holds (p + q) . x = (p . x) + (q . x)