theorem Th79: :: PDIFF_9:79

for m being non zero Element of NAT
for X being Subset of (REAL m)
for r being Real
for I being non empty FinSequence of NAT
for f being PartFunc of (REAL m),REAL st X is open & rng I c= Seg m & 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)) )