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`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:]; 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; ( 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
; ( 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 2;
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:];
( 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
;
( 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;
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; (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;
( 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;
then P10: dom ((f `partial`2| Z) - (g `partial`2| Z)) =
Z /\ Z
by P8, VFUNCT_1:def 2
.=
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:];
( x in Z implies ((f `partial`2| Z) - (g `partial`2| Z)) /. x = partdiff`2 ((f - g),x) )
assume P11:
x in Z
;
((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 2
.=
partdiff`2 (
(f - g),
x)
by P11, X1, Z1, Z2
;
verum
end;
hence
(f - g) `partial`2| Z = (f `partial`2| Z) - (g `partial`2| Z)
by P7, P10, Def92; verum