theorem
for
f being
PartFunc of
(REAL 3),
REAL for
u0 being
Element of
REAL 3
for
N being
Neighbourhood of
(proj (2,3)) . u0 st
f is_hpartial_differentiable`12_in u0 &
N c= dom (SVF1 (2,(pdiff1 (f,1)),u0)) holds
for
h being
non-zero 0 -convergent Real_Sequence for
c being
constant Real_Sequence st
rng c = {((proj (2,3)) . u0)} &
rng (h + c) c= N holds
(
(h ") (#) (((SVF1 (2,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),u0)) /* c)) is
convergent &
hpartdiff12 (
f,
u0)
= lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,1)),u0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,1)),u0)) /* c))) )