theorem Th54: :: AFINSQ_2:55

for cF1, cF2 being complex-valued XFinSequence holds Sum (cF1 ^ cF2) = (Sum cF1) + (Sum cF2)