theorem :: RVSUM_2:41

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