theorem :: FDIFF_12:52

for f1, f2 being PartFunc of REAL,REAL
for I, J being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval J & f1 .: I c= J holds
( f2 * f1 is_differentiable_on_interval I & (f2 * f1) `\ I = ((f2 `\ J) * f1) (#) (f1 `\ I) )