let n be 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)) ) )
let Z be 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)) ) )
let f1, f2 be PartFunc of REAL,(REAL n); ( 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)) ) )
reconsider g1 = f1, g2 = f2 as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A3:
f1 + f2 = g1 + g2
by NFCONT_4:5;
A4:
Z c= dom (g1 + g2)
by A1, NFCONT_4:5;
A5:
( Z c= dom g1 & Z c= dom g2 )
by A2;
then A6:
g1 is_differentiable_on Z
by A5, NDIFF_3:def 5;
then
g2 is_differentiable_on Z
by A5, NDIFF_3:def 5;
then A7:
( g1 + g2 is_differentiable_on Z & ( for x being Real st x in Z holds
((g1 + g2) `| Z) . x = (diff (g1,x)) + (diff (g2,x)) ) )
by A4, A6, NDIFF_3:17;
hence A8:
f1 + f2 is_differentiable_on Z
by A1; 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 A9:
x in Z
; ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
then
( f1 is_differentiable_in x & f2 is_differentiable_in x )
by A2, Th5;
then
( f1 + f2 is_differentiable_in x & diff ((f1 + f2),x) = (diff (f1,x)) + (diff (f2,x)) )
by Th11;
hence
((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x))
by A9, A8, Def4; verum