theorem :: FDIFF_12:23

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