let S be RealNormSpace-Sequence; :: thesis: for T being RealNormSpace
for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )
let T be RealNormSpace; :: thesis: for Z being Subset of (product S)
for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )
let Z be Subset of (product S); :: thesis: for f, g being PartFunc of (product S),T
for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )
let f, g be PartFunc of (product S),T; :: thesis: for i being set st Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i holds
( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )
let i be set ; :: thesis: ( Z is open & i in dom S & f is_partial_differentiable_on Z,i & g is_partial_differentiable_on Z,i implies ( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) ) )
assume that
A1: ( Z is open & i in dom S ) and
A2: f is_partial_differentiable_on Z,i and
A3: g is_partial_differentiable_on Z,i ; :: thesis: ( f + g is_partial_differentiable_on Z,i & (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) )
A4: ( Z c= dom f & Z c= dom g ) by A2, A3, NDIFF_5:def 8;
then Z c= (dom f) /\ (dom g) by XBOOLE_1:19;
then A5: Z c= dom (f + g) by VFUNCT_1:def 1;
then A9: dom ((f + g) | Z) = Z by RELAT_1:62;
for x being Point of (product S) st x in Z holds
(f + g) | Z is_partial_differentiable_in x,i

proof

let x be Point of (product S); :: thesis: ( x in Z implies (f + g) | Z is_partial_differentiable_in x,i )
assume x in Z ; :: thesis: (f + g) | Z is_partial_differentiable_in x,i
then ( f | Z is_partial_differentiable_in x,i & g | Z is_partial_differentiable_in x,i ) by A2, A3, NDIFF_5:def 8;
then A6: (f | Z) + (g | Z) is_partial_differentiable_in x,i by A1, NDIFF_5:28;
A7: ( dom (f | Z) = Z & dom (g | Z) = Z ) by A4, RELAT_1:62;
then A8: (dom (f | Z)) /\ (dom (g | Z)) = Z ;
for x being Element of (product S) st x in dom ((f + g) | Z) holds
((f + g) | Z) /. x = ((f | Z) /. x) + ((g | Z) /. x)

proof

let x be Element of (product S); :: thesis: ( x in dom ((f + g) | Z) implies ((f + g) | Z) /. x = ((f | Z) /. x) + ((g | Z) /. x) )
assume A10: x in dom ((f + g) | Z) ; :: thesis: ((f + g) | Z) /. x = ((f | Z) /. x) + ((g | Z) /. x)
hence ((f + g) | Z) /. x = (f + g) /. x by PARTFUN1:80
.= (f /. x) + (g /. x) by A5, A9, A10, VFUNCT_1:def 1
.= ((f | Z) /. x) + (g /. x) by A7, A10, PARTFUN1:80
.= ((f | Z) /. x) + ((g | Z) /. x) by A7, A10, PARTFUN1:80 ;
:: thesis: verum

end;

hence (f + g) | Z is_partial_differentiable_in x,i by A5, A6, A8, RELAT_1:62, VFUNCT_1:def 1; :: thesis: verum

end;

hence A11: f + g is_partial_differentiable_on Z,i by A5, NDIFF_5:def 8; :: thesis: (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i))
set pfg = (f `partial| (Z,i)) + (g `partial| (Z,i));
( dom (f `partial| (Z,i)) = Z & dom (g `partial| (Z,i)) = Z ) by A2, A3, NDIFF_5:def 9;
then (dom (f `partial| (Z,i))) /\ (dom (g `partial| (Z,i))) = Z ;
then A12: dom ((f `partial| (Z,i)) + (g `partial| (Z,i))) = Z by VFUNCT_1:def 1;
for x being Point of (product S) st x in Z holds
((f `partial| (Z,i)) + (g `partial| (Z,i))) /. x = partdiff ((f + g),x,i)

proof

let x be Point of (product S); :: thesis: ( x in Z implies ((f `partial| (Z,i)) + (g `partial| (Z,i))) /. x = partdiff ((f + g),x,i) )
assume A13: x in Z ; :: thesis: ((f `partial| (Z,i)) + (g `partial| (Z,i))) /. x = partdiff ((f + g),x,i)
then A14: ( f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i ) by A1, A2, A3, NDIFF_5:32;
thus ((f `partial| (Z,i)) + (g `partial| (Z,i))) /. x = ((f `partial| (Z,i)) /. x) + ((g `partial| (Z,i)) /. x) by A12, A13, VFUNCT_1:def 1
.= (partdiff (f,x,i)) + ((g `partial| (Z,i)) /. x) by A2, A13, NDIFF_5:def 9
.= (partdiff (f,x,i)) + (partdiff (g,x,i)) by A3, A13, NDIFF_5:def 9
.= partdiff ((f + g),x,i) by A1, A14, NDIFF_5:28 ; :: thesis: verum

end;

hence (f + g) `partial| (Z,i) = (f `partial| (Z,i)) + (g `partial| (Z,i)) by A11, A12, NDIFF_5:def 9; :: thesis: verum