let X, Y, W be RealNormSpace; :: thesis: 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`2 Z & g is_partial_differentiable_on`2 Z holds
( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) )
let Z be Subset of [:X,Y:]; :: thesis: for f, g being PartFunc of [:X,Y:],W st Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z holds
( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) )
let f, g be PartFunc of [:X,Y:],W; :: thesis: ( Z is open & f is_partial_differentiable_on`2 Z & g is_partial_differentiable_on`2 Z implies ( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) ) )
assume that
O1: Z is open and
A1: f is_partial_differentiable_on`2 Z and
A2: g is_partial_differentiable_on`2 Z ; :: thesis: ( f + g is_partial_differentiable_on`2 Z & (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| 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`2 x & partdiff`2 ((f + g),x) = (partdiff`2 (f,x)) + (partdiff`2 (g,x)) )

proof

let x be Point of [:X,Y:]; :: thesis: ( x in Z implies ( f + g is_partial_differentiable_in`2 x & partdiff`2 ((f + g),x) = (partdiff`2 (f,x)) + (partdiff`2 (g,x)) ) )
assume P5: x in Z ; :: thesis: ( f + g is_partial_differentiable_in`2 x & partdiff`2 ((f + g),x) = (partdiff`2 (f,x)) + (partdiff`2 (g,x)) )
then P6: f is_partial_differentiable_in`2 x by A1, O1, NDIFF5242;
g is_partial_differentiable_in`2 x by A2, O1, P5, NDIFF5242;
hence ( f + g is_partial_differentiable_in`2 x & partdiff`2 ((f + g),x) = (partdiff`2 (f,x)) + (partdiff`2 (g,x)) ) by LM216, P6; :: thesis: verum

end;

then for x being Point of [:X,Y:] st x in Z holds
f + g is_partial_differentiable_in`2 x ;
hence P7: f + g is_partial_differentiable_on`2 Z by NDIFF5242, D1, O1; :: thesis: (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z)
set fp = f `partial`2| Z;
set gp = g `partial`2| Z;
P8: ( dom (f `partial`2| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(f `partial`2| Z) /. x = partdiff`2 (f,x) ) ) by A1, Def92;
P9: ( dom (g `partial`2| Z) = Z & ( for x being Point of [:X,Y:] st x in Z holds
(g `partial`2| Z) /. x = partdiff`2 (g,x) ) ) by A2, Def92;
P10: dom ((f `partial`2| Z) + (g `partial`2| 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`2| Z) + (g `partial`2| Z)) /. x = partdiff`2 ((f + g),x)

proof

let x be Point of [:X,Y:]; :: thesis: ( x in Z implies ((f `partial`2| Z) + (g `partial`2| Z)) /. x = partdiff`2 ((f + g),x) )
assume P11: x in Z ; :: thesis: ((f `partial`2| Z) + (g `partial`2| Z)) /. x = partdiff`2 ((f + g),x)
then Z1: (f `partial`2| Z) /. x = partdiff`2 (f,x) by A1, Def92;
Z2: (g `partial`2| Z) /. x = partdiff`2 (g,x) by A2, P11, Def92;
thus ((f `partial`2| Z) + (g `partial`2| Z)) /. x = ((f `partial`2| Z) /. x) + ((g `partial`2| Z) /. x) by P11, P10, VFUNCT_1:def 1
.= partdiff`2 ((f + g),x) by P11, X1, Z1, Z2 ; :: thesis: verum

end;

hence (f + g) `partial`2| Z = (f `partial`2| Z) + (g `partial`2| Z) by P7, P10, Def92; :: thesis: verum