let X, Y, W be RealNormSpace; for Z being Subset of [:X,Y:]
for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds
( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )
let Z be Subset of [:X,Y:]; for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z holds
( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )
let f, g be PartFunc of [:X,Y:],W; ( Z is open & f is_partial_differentiable_on`1 Z & g is_partial_differentiable_on`1 Z implies ( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) ) )
assume that
O1:
Z is open
and
A1:
f is_partial_differentiable_on`1 Z
and
A2:
g is_partial_differentiable_on`1 Z
; ( f + g is_partial_differentiable_on`1 Z & (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z) )
set h = f + g;
dom (f + g) = (dom f) /\ (dom g)
by VFUNCT_1:def 1;
then D1:
Z c= dom (f + g)
by A1, A2, XBOOLE_1:19;
X1:
for x being Point of [:X,Y:] st x in Z holds
( f + g is_partial_differentiable_in`1 x & partdiff`1 ((f + g),x) = (partdiff`1 (f,x)) + (partdiff`1 (g,x)) )
proof
let x be
Point of
[:X,Y:];
( x in Z implies ( f + g is_partial_differentiable_in`1 x & partdiff`1 ((f + g),x) = (partdiff`1 (f,x)) + (partdiff`1 (g,x)) ) )
assume P5:
x in Z
;
( f + g is_partial_differentiable_in`1 x & partdiff`1 ((f + g),x) = (partdiff`1 (f,x)) + (partdiff`1 (g,x)) )
then P6:
f is_partial_differentiable_in`1 x
by A1, O1, NDIFF5241;
g is_partial_differentiable_in`1 x
by A2, O1, P5, NDIFF5241;
hence
(
f + g is_partial_differentiable_in`1 x &
partdiff`1 (
(f + g),
x)
= (partdiff`1 (f,x)) + (partdiff`1 (g,x)) )
by LM215, P6;
verum
end;
then
for x being Point of [:X,Y:] st x in Z holds
f + g is_partial_differentiable_in`1 x
;
hence P7:
f + g is_partial_differentiable_on`1 Z
by NDIFF5241, D1, O1; (f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z)
set fp = f `partial`1| Z;
set gp = g `partial`1| Z;
P8:
( dom (f `partial`1| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(f `partial`1| Z) /. x = partdiff`1 (f,x) ) )
by A1, Def91;
P9:
( dom (g `partial`1| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(g `partial`1| Z) /. x = partdiff`1 (g,x) ) )
by A2, Def91;
P10: dom ((f `partial`1| Z) + (g `partial`1| Z)) =
Z /\ Z
by P8, P9, VFUNCT_1:def 1
.=
Z
;
for x being Point of [:X,Y:] st x in Z holds
((f `partial`1| Z) + (g `partial`1| Z)) /. x = partdiff`1 ((f + g),x)
proof
let x be
Point of
[:X,Y:];
( x in Z implies ((f `partial`1| Z) + (g `partial`1| Z)) /. x = partdiff`1 ((f + g),x) )
assume P11:
x in Z
;
((f `partial`1| Z) + (g `partial`1| Z)) /. x = partdiff`1 ((f + g),x)
Z1:
(f `partial`1| Z) /. x = partdiff`1 (
f,
x)
by A1, P11, Def91;
Z2:
(g `partial`1| Z) /. x = partdiff`1 (
g,
x)
by A2, P11, Def91;
thus ((f `partial`1| Z) + (g `partial`1| Z)) /. x =
((f `partial`1| Z) /. x) + ((g `partial`1| Z) /. x)
by P11, P10, VFUNCT_1:def 1
.=
partdiff`1 (
(f + g),
x)
by P11, X1, Z1, Z2
;
verum
end;
hence
(f + g) `partial`1| Z = (f `partial`1| Z) + (g `partial`1| Z)
by P7, P10, Def91; verum