theorem Th27: :: RVSUM_2:27

for i being Nat
for c being Complex
for R being b₁ -element complex-valued FinSequence holds mlt ((i |-> c),R) = c * R