theorem Th21: :: POLYNOM1:21

for n being set
for L being non empty add-associative right_zeroed doubleLoopStr
for p, q, r being Series of n,L holds (p + q) + r = p + (q + r)