theorem Th22:
for
m,
n being non
zero Element of
NAT for
f being
PartFunc of
(REAL m),
(REAL n) for
g being
PartFunc of
(REAL-NS m),
(REAL-NS n) for
X being
Subset of
(REAL m) for
Y being
Subset of
(REAL-NS m) for
i being
Nat st 1
<= i &
i <= m &
X is
open &
g = f &
X = Y &
f is_partial_differentiable_on X,
i holds
for
x0,
x1 being
Element of
REAL m for
y0,
y1 being
Point of
(REAL-NS m) st
x0 = y0 &
x1 = y1 &
x0 in X &
x1 in X holds
|.(((f `partial| (X,i)) /. x1) - ((f `partial| (X,i)) /. x0)).| = ||.(((g `partial| (Y,i)) /. y1) - ((g `partial| (Y,i)) /. y0)).||