theorem :: NDIFF_3:17

for F being RealNormSpace
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) ) )