theorem :: NDIFF_1:39

for S, T being RealNormSpace
for Z being Subset of S st Z is open holds
for f1, f2 being PartFunc of S,T 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 Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )