theorem :: CFDIFF_1:28

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