theorem :: FDIFF_12:19

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