for S, T being RealNormSpace
for r being Real
for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
( r (#) f is_differentiable_in x0 & diff ((r (#) f),x0) = r * (diff (f,x0)) )