for n, m being non zero Element of NAT
for x0 being Element of REAL
for g being PartFunc of REAL,(REAL-NS n) st g is_differentiable_in x0 holds
for f being PartFunc of (REAL-NS n),(REAL-NS m) st f is_differentiable_in g /. x0 holds
( f * g is_differentiable_in x0 & diff ((f * g),x0) = (diff (f,(g /. x0))) . (diff (g,x0)) )