for X, Y, W being RealNormSpace
for Z being Subset of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z holds
( r (#) f is_partial_differentiable_on`2 Z & (r (#) f) `partial`2| Z = r (#) (f `partial`2| Z) )