theorem :: VFUNCT_1:31

for X being set
for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real holds (r (#) f) | X = r (#) (f | X)