theorem Th41: :: MESFUN6C:41

for X being non empty set
for f being PartFunc of X,REAL
for Y being set
for r being Real holds (r (#) f) | Y = r (#) (f | Y)