theorem Th52: :: PDIFF_9:52

for m being non zero Element of NAT
for f being PartFunc of (REAL m),REAL
for r being Real
for x being Element of REAL m st f is_differentiable_in x holds
( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r (#) (diff (f,x)) )