let m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
let i be Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
let X be Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),REAL st X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i holds
( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i implies ( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) ) )
assume AS: ( X is open & 1 <= i & i <= m & f is_partial_differentiable_on X,i & g is_partial_differentiable_on X,i ) ; :: thesis: ( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
P1: ( X c= dom f & X c= dom g ) by AS, PDIFF734;
Q1: ( dom (f `partial| (X,i)) = X & dom (g `partial| (X,i)) = X ) by DefPDX, AS;
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then P3: X c= dom (f + g) by P1, XBOOLE_1:19;

XX1: now :: thesis: for x being Element of REAL m st x in X holds
( f + g is_partial_differentiable_in x,i & partdiff ((f + g),x,i) = (partdiff (f,x,i)) + (partdiff (g,x,i)) )

let x be Element of REAL m; :: thesis: ( x in X implies ( f + g is_partial_differentiable_in x,i & partdiff ((f + g),x,i) = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) )
assume x in X ; :: thesis: ( f + g is_partial_differentiable_in x,i & partdiff ((f + g),x,i) = (partdiff (f,x,i)) + (partdiff (g,x,i)) )
then ( f is_partial_differentiable_in x,i & g is_partial_differentiable_in x,i ) by AS, PDIFF734;
hence ( f + g is_partial_differentiable_in x,i & partdiff ((f + g),x,i) = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) by PDIFF_1:29; :: thesis: verum

end;

then P7: for x being Element of REAL m st x in X holds
f + g is_partial_differentiable_in x,i ;
then P8: f + g is_partial_differentiable_on X,i by P3, PDIFF734, AS;
then P9: dom ((f + g) `partial| (X,i)) = X by DefPDX;

P10: now :: thesis: for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i))

let x be Element of REAL m; :: thesis: ( x in X implies ((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) )
assume P10: x in X ; :: thesis: ((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i))
then ((f + g) `partial| (X,i)) /. x = partdiff ((f + g),x,i) by P8, DefPDX;
hence ((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) by XX1, P10; :: thesis: verum

end;

P11: dom ((f `partial| (X,i)) + (g `partial| (X,i))) = (dom (f `partial| (X,i))) /\ (dom (g `partial| (X,i))) by VALUED_1:def 1;

now :: thesis: for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) . x = ((f `partial| (X,i)) + (g `partial| (X,i))) . x

let x be Element of REAL m; :: thesis: ( x in X implies ((f + g) `partial| (X,i)) . x = ((f `partial| (X,i)) + (g `partial| (X,i))) . x )
assume A1: x in X ; :: thesis: ((f + g) `partial| (X,i)) . x = ((f `partial| (X,i)) + (g `partial| (X,i))) . x
thus ((f + g) `partial| (X,i)) . x = ((f + g) `partial| (X,i)) /. x by A1, P9, PARTFUN1:def 6
.= (partdiff (f,x,i)) + (partdiff (g,x,i)) by P10, A1
.= ((f `partial| (X,i)) /. x) + (partdiff (g,x,i)) by A1, DefPDX, AS
.= ((f `partial| (X,i)) /. x) + ((g `partial| (X,i)) /. x) by A1, DefPDX, AS
.= ((f `partial| (X,i)) . x) + ((g `partial| (X,i)) /. x) by A1, Q1, PARTFUN1:def 6
.= ((f `partial| (X,i)) . x) + ((g `partial| (X,i)) . x) by A1, Q1, PARTFUN1:def 6
.= ((f `partial| (X,i)) + (g `partial| (X,i))) . x by A1, P11, Q1, VALUED_1:def 1 ; :: thesis: verum

end;

hence ( f + g is_partial_differentiable_on X,i & (f + g) `partial| (X,i) = (f `partial| (X,i)) + (g `partial| (X,i)) & ( for x being Element of REAL m st x in X holds
((f + g) `partial| (X,i)) /. x = (partdiff (f,x,i)) + (partdiff (g,x,i)) ) ) by P7, P3, PDIFF734, AS, P9, P10, P11, Q1, PARTFUN1:5; :: thesis: verum