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