theorem Th9: :: NDIFF_4:9

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