theorem :: VFUNCT_1:39

for C being non empty set
for c being Element of C
for V being RealNormSpace
for f being PartFunc of C,V
for r being Real st f is total holds
(r (#) f) /. c = r * (f /. c)