for r being R_eal
for F being FinSequence of ExtREAL holds Sum (F ^ <*r*>) = (Sum F) + r