theorem Th40: :: RVSUM_2:40

for i being Nat
for R1, R2 being b₁ -element complex-valued FinSequence holds Sum (R1 + R2) = (Sum R1) + (Sum R2)