for m, n being non zero Element of NAT
for X being Subset of (REAL m)
for f being PartFunc of (REAL m),(REAL n)
for r being Real st f is_differentiable_on X holds
( r (#) f is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((r (#) f) `| X) /. x = r (#) (diff (f,x)) ) )