:: deftheorem defines + POLYNOM1:def 6 :
for n being set
for L being non empty addLoopStr
for p, q being Series of n,L holds p + q = p + q;