theorem :: MESFUN7C:28

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