theorem :: FDIFF_12:24

for f1, f2 being PartFunc of REAL,REAL
for I being non empty Interval st f1 is_differentiable_on_interval I & f2 is_differentiable_on_interval I holds
( f1 (#) f2 is_differentiable_on_interval I & (f1 (#) f2) `\ I = (f2 (#) (f1 `\ I)) + (f1 (#) (f2 `\ I)) & ( for x being Real st x in I holds
((f1 (#) f2) `\ I) . x = ((f2 . x) * ((f1 `\ I) . x)) + ((f1 . x) * ((f2 `\ I) . x)) ) )