theorem :: RVSUM_2:41
for i being Nat
for R1, R2 being b1 -element FinSequence of COMPLEX holds Sum (R1 - R2) = (Sum R1) - (Sum R2)