theorem Th24: :: POLYNOM3:26

for L being non empty add-associative addLoopStr
for p, q, r being sequence of L holds (p + q) + r = p + (q + r)