theorem Th20: :: MEASURE9:22

for r being R_eal
for i being Nat st r is real holds
Sum (i |-> r) = i * r