theorem SPP: :: RVSUM_4:49

for n being Nat
for f1, f2 being b₁ -element complex-valued XFinSequence holds Sum (f1 + f2) = (Sum f1) + (Sum f2)