let m, n be non zero Element of NAT ; for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) )
let X be Subset of (REAL m); for f, g being PartFunc of (REAL m),(REAL n) st f is_differentiable_on X & g is_differentiable_on X holds
( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) )
let f, g be PartFunc of (REAL m),(REAL n); ( f is_differentiable_on X & g is_differentiable_on X implies ( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) ) )
assume A1:
( f is_differentiable_on X & g is_differentiable_on X )
; ( f + g is_differentiable_on X & ( for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) ) )
then A2:
X is open
by PDIFF_6:33;
then A3:
( X c= dom f & X c= dom g )
by A1, Th14;
dom (f + g) = (dom f) /\ (dom g)
by VALUED_2:def 45;
then A4:
X c= dom (f + g)
by A3, XBOOLE_1:19;
hence
f + g is_differentiable_on X
by A4, A2, Th14; for x being Element of REAL m st x in X holds
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x))
let x be Element of REAL m; ( x in X implies ((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x)) )
assume A5:
x in X
; ((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x))
then
( f is_differentiable_in x & g is_differentiable_in x )
by A1, A2, Th14;
then
diff ((f + g),x) = (diff (f,x)) + (diff (g,x))
by PDIFF_6:20;
hence
((f + g) `| X) /. x = (diff (f,x)) + (diff (g,x))
by A4, A5, Def1; verum