theorem Th80: :: RVSUM_1:80

for i being natural Number
for r being Real holds Sum (i |-> r) = i * r