theorem LM217: :: NDIFF_7:38

for X, Y, W being RealNormSpace
for z being Point of [:X,Y:]
for r being Real
for f being PartFunc of [:X,Y:],W st f is_partial_differentiable_in`1 z holds
( r (#) f is_partial_differentiable_in`1 z & partdiff`1 ((r (#) f),z) = r * (partdiff`1 (f,z)) )