let S, T be non trivial RealNormSpace; :: thesis:
let Z be Subset of S; :: thesis:
assume A1: Z is open ; :: thesis:
let f1, f2 be PartFunc of S,T; :: thesis:
assume that
A2: Z c= dom (f1 + f2) and
A3: f1 is_differentiable_on Z and
A4: f2 is_differentiable_on Z ; :: thesis:

let x0 be Point of S; :: thesis:
assume A5: x0 in Z ; :: thesis:
then A6: f1 is_differentiable_in x0 by A1, A3, Th36;
f2 is_differentiable_in x0 by A1, A4, A5, Th36;
hence f1 + f2 is_differentiable_in x0 by A6, Th40; :: thesis:

end;

hence A7: f1 + f2 is_differentiable_on Z by A1, A2, Th36; :: thesis:

let x be Point of S; :: thesis:
assume A8: x in Z ; :: thesis:
then A9: f1 is_differentiable_in x by A1, A3, Th36;
A10: f2 is_differentiable_in x by A1, A4, A8, Th36;
thus ((f1 + f2) `| Z) /. x = diff (f1 + f2),x by A7, A8, Def9
.= (diff f1,x) + (diff f2,x) by A9, A10, Th40 ; :: thesis:

end;

hence for x being Point of S st x in Z holds
((f1 + f2) `| Z) /. x = (diff f1,x) + (diff f2,x) ; :: thesis: