theorem Th3: :: E_TRANS2:1

for i being Nat
for r being Element of F_Real holds Sum (i |-> r) = i * r