theorem :: RVSUM_2:18

for i being Nat
for R1, R2 being b₁ -element complex-valued FinSequence st R1 - R2 = i |-> 0c holds
R1 = R2