theorem :: PDIFF_6:22

for n, m being non zero Nat
for g being PartFunc of (REAL m),(REAL n)
for y0 being Element of REAL m
for r being Real st g is_differentiable_in y0 holds
( r (#) g is_differentiable_in y0 & diff ((r (#) g),y0) = r (#) (diff (g,y0)) )