let f be PartFunc of (REAL 3),REAL; for u being Element of REAL 3 holds
( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
let u be Element of REAL 3; ( f is_partial_differentiable_in u,2 iff ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) )
hereby ( ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) implies f is_partial_differentiable_in u,2 )
assume A1:
f is_partial_differentiable_in u,2
;
ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )thus
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,u)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
y being
Real st
y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
verumproof
consider x0,
y0,
z0 being
Real such that A2:
(
u = <*x0,y0,z0*> &
SVF1 (2,
f,
u)
is_differentiable_in y0 )
by A1, Th8;
ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,u)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
y being
Real st
y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
by A2, FDIFF_1:def 4;
hence
ex
x0,
y0,
z0 being
Real st
(
u = <*x0,y0,z0*> & ex
N being
Neighbourhood of
y0 st
(
N c= dom (SVF1 (2,f,u)) & ex
L being
LinearFunc ex
R being
RestFunc st
for
y being
Real st
y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
by A2;
verum
end;
end;
assume
ex x0, y0, z0 being Real st
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
; f is_partial_differentiable_in u,2
then consider x0, y0, z0 being Real such that
A3:
( u = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) ) )
;
consider N being Neighbourhood of y0 such that
A4:
( N c= dom (SVF1 (2,f,u)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,f,u)) . y) - ((SVF1 (2,f,u)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
by A3;
SVF1 (2,f,u) is_differentiable_in y0
by A4, FDIFF_1:def 4;
hence
f is_partial_differentiable_in u,2
by A3, Th8; verum