let G be RealNormSpace-Sequence; 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; 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 ; 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; 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); ( 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
; ( 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);
( 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
;
( 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;
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; (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);
( x in X implies ((f `partial| (X,i)) - (g `partial| (X,i))) /. x = partdiff ((f - g),x,i) )
assume P11:
x in X
;
((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
;
verum
end;
hence
(f - g) `partial| (X,i) = (f `partial| (X,i)) - (g `partial| (X,i))
by P7, P10, NDIFF_5:def 9; verum