theorem :: RVSUM_2:15

for i being Nat
for R being b₁ -element FinSequence of COMPLEX holds R - (i |-> 0c) = R