let G be RealNormSpace-Sequence; :: thesis: for F being RealNormSpace
for i being set
for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let F be RealNormSpace; :: thesis: for i being set
for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let i be set ; :: thesis: for f, g being PartFunc of (product G),F
for X being Subset of (product G) st X is open & i in dom G & 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)) )
let f, g be PartFunc of (product G),F; :: thesis: for X being Subset of (product G) st X is open & i in dom G & 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)) )
let X be Subset of (product G); :: thesis: ( X is open & i in dom G & 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)) ) )
assume that
O1: X is open and
A0: i in dom G and
A1: f is_partial_differentiable_on X,i and
A2: 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)) )
set h = f - g;
dom (f - g) = (dom f) /\ (dom g) by VFUNCT_1:def 2;
then D1: X c= dom (f - g) by A1, A2, XBOOLE_1:19;
X1: for x being Point of (product G) 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)) )

proof

let x be Point of (product G); :: 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 P5: 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 P6: f is_partial_differentiable_in x,i by A1, O1, NDIFF_5:24;
g is_partial_differentiable_in x,i by A2, O1, P5, NDIFF_5:24;
hence ( f - g is_partial_differentiable_in x,i & partdiff ((f - g),x,i) = (partdiff (f,x,i)) - (partdiff (g,x,i)) ) by A0, NDIFF_5:29, P6; :: thesis: verum

end;

then for x being Point of (product G) st x in X holds
f - g is_partial_differentiable_in x,i ;
hence P7: f - g is_partial_differentiable_on X,i by NDIFF_5:24, D1, O1; :: thesis: (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i))
set fp = f `partial| (X,i);
set gp = g `partial| (X,i);
P8: ( dom (f `partial| (X,i)) = X & ( for x being Point of (product G) st x in X holds
(f `partial| (X,i)) /. x = partdiff (f,x,i) ) ) by A1, NDIFF_5:def 9;
P9: ( dom (g `partial| (X,i)) = X & ( for x being Point of (product G) st x in X holds
(g `partial| (X,i)) /. x = partdiff (g,x,i) ) ) by A2, NDIFF_5:def 9;
P10: dom ((f `partial| (X,i)) - (g `partial| (X,i))) = X /\ X by P8, P9, VFUNCT_1:def 2
.= X ;
for x being Point of (product G) st x in X holds
((f `partial| (X,i)) - (g `partial| (X,i))) /. x = partdiff ((f - g),x,i)

proof

let x be Point of (product G); :: thesis: ( x in X implies ((f `partial| (X,i)) - (g `partial| (X,i))) /. x = partdiff ((f - g),x,i) )
assume P11: x in X ; :: thesis: ((f `partial| (X,i)) - (g `partial| (X,i))) /. x = partdiff ((f - g),x,i)
Z1: (f `partial| (X,i)) /. x = partdiff (f,x,i) by A1, P11, NDIFF_5:def 9;
thus ((f `partial| (X,i)) - (g `partial| (X,i))) /. x = ((f `partial| (X,i)) /. x) - ((g `partial| (X,i)) /. x) by P11, P10, VFUNCT_1:def 2
.= (partdiff (f,x,i)) - (partdiff (g,x,i)) by Z1, A2, P11, NDIFF_5:def 9
.= partdiff ((f - g),x,i) by P11, X1 ; :: thesis: verum

end;

hence (f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i)) by P7, P10, NDIFF_5:def 9; :: thesis: verum