theorem Th19: :: MEASURE9:21
for r being R_eal
for F being FinSequence of ExtREAL holds Sum (F ^ <*r*>) = (Sum F) + r