for r being Real
for A being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on A holds
( r (#) f is_differentiable_on A & (r (#) f) `| A = r (#) (f `| A) )