theorem Th67: :: PDIFF_9:67

for m being non zero Element of NAT
for i being Element of NAT
for X being Subset of (REAL m)
for r being Real
for f being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= 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)) & ( for x being Element of REAL m st x in X holds
((r (#) f) `partial| (X,i)) /. x = r * (partdiff (f,x,i)) ) )