theorem :: RFUNCT_3:80

for D being non empty set
for F being PartFunc of D,REAL
for X being set
for r being Real
for Y being finite set st Y = dom (F | X) holds
Sum ((F - r),X) = (Sum (F,X)) - (r * (card Y))