theorem :: CFUNCT_1:65

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