for S, T being RealNormSpace
for x0 being Point of S
for U being RealNormSpace
for f1 being PartFunc of S,T st f1 is_differentiable_in x0 holds
for f2 being PartFunc of T,U st f2 is_differentiable_in f1 /. x0 holds
( f2 * f1 is_differentiable_in x0 & diff ((f2 * f1),x0) = (diff (f2,(f1 /. x0))) * (diff (f1,x0)) )