theorem Th19: :: POLYFORM:21

for p, q, r being complex-valued FinSequence holds Sum ((p ^ q) ^ r) = ((Sum p) + (Sum q)) + (Sum r)