theorem Th75: :: RVSUM_1:75

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