theorem :: CFUNCT_1:57

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