theorem
for
x0,
y0,
z0 being
Real for
u being
Element of
REAL 3
for
f being
PartFunc of
(REAL 3),
REAL st
u = <*x0,y0,z0*> &
f is_partial_differentiable_in u,1 holds
ex
N being
Neighbourhood of
x0 st
(
N c= dom (SVF1 (1,f,u)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
x being
Real st
x in N holds
((SVF1 (1,f,u)) . x) - ((SVF1 (1,f,u)) . x0) = (L . (x - x0)) + (R . (x - x0)) )