theorem Th36: :: RVSUM_2:36

for i being Nat
for c being Complex holds Sum (i |-> c) = i * c