let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL 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) ) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( 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) ) ) )
assume that
A1: Z c= dom (f1 + f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; :: thesis: ( 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) ) )

now

let x0 be Real; :: thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 )
assume x0 in Z ; :: thesis: f1 + f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th16;
hence f1 + f2 is_differentiable_in x0 by Th21; :: thesis: verum

end;

hence A3: f1 + f2 is_differentiable_on Z by A1, Th16; :: thesis: for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff f1,x) + (diff f2,x)

now

let x be Real; :: thesis: ( x in Z implies ((f1 + f2) `| Z) . x = (diff f1,x) + (diff f2,x) )
assume A4: x in Z ; :: thesis: ((f1 + f2) `| Z) . x = (diff f1,x) + (diff f2,x)
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th16;
thus ((f1 + f2) `| Z) . x = diff (f1 + f2),x by A3, A4, Def8
.= (diff f1,x) + (diff f2,x) by A5, Th21 ; :: thesis: verum

end;

hence for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff f1,x) + (diff f2,x) ; :: thesis: verum