let F be RealNormSpace; for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL, the carrier of F 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 Z be open Subset of REAL; for f1, f2 being PartFunc of REAL, the carrier of F 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, the carrier of F; ( 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 )
; ( 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)) ) )
hence A3:
f1 + f2 is_differentiable_on Z
by A1, Th10; for x being Real st x in Z holds
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
let x be Real; ( x in Z implies ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) )
assume A4:
x in Z
; ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
then A5:
( f1 is_differentiable_in x & f2 is_differentiable_in x )
by A2, Th10;
thus ((f1 + f2) `| Z) . x =
diff ((f1 + f2),x)
by A3, A4, Def6
.=
(diff (f1,x)) + (diff (f2,x))
by A5, Th14
; verum