theorem Th77: :: RFUNCT_3:77

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