theorem :: NDIFF_7:25

for G being RealNormSpace-Sequence
for F being RealNormSpace
for i being set
for f being PartFunc of (product G),F
for r being Real
for X being Subset of (product G) st X is open & i in dom G & f is_partial_differentiable_on X,i holds
( r (#) f is_partial_differentiable_on X,i & (r (#) f) `partial| (X,i) = r (#) (f `partial| (X,i)) )