theorem :: RVSUM_2:24

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