theorem :: RVSUM_1:73

for r being Real holds Sum <*r*> = r