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