theorem Th15: :: NDIFF_4:15

for n being non zero Element of NAT
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,(REAL n) 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)) ) )