theorem Th32: :: RVSUM_2:32

for F1, F2 being complex-valued FinSequence holds Sum (F1 ^ F2) = (Sum F1) + (Sum F2)