let Z be Subset of (REAL 2); for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`2_on Z holds
( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
let f be PartFunc of (REAL 2),REAL; ( f is_partial_differentiable`2_on Z implies ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) ) )
set g = f | Z;
assume A1:
f is_partial_differentiable`2_on Z
; ( Z c= dom f & ( for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2 ) )
hence
Z c= dom f
; for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,2
let z0 be Element of REAL 2; ( z0 in Z implies f is_partial_differentiable_in z0,2 )
assume
z0 in Z
; f is_partial_differentiable_in z0,2
then
f | Z is_partial_differentiable_in z0,2
by A1;
then consider x0, y0 being Real such that
A2:
z0 = <*x0,y0*>
and
A3:
ex N being Neighbourhood of y0 st
( N c= dom (SVF1 (2,(f | Z),z0)) & ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
by Th10;
consider N being Neighbourhood of y0 such that
A4:
N c= dom (SVF1 (2,(f | Z),z0))
and
A5:
ex L being LinearFunc ex R being RestFunc st
for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
by A3;
consider L being LinearFunc, R being RestFunc such that
A6:
for y being Real st y in N holds
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
by A5;
A7:
for y being Real st y in N holds
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
proof
let y be
Real;
( y in N implies ((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0)) )
A8:
for
y being
Real st
y in dom (SVF1 (2,(f | Z),z0)) holds
(SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y
proof
let y be
Real;
( y in dom (SVF1 (2,(f | Z),z0)) implies (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y )
assume A9:
y in dom (SVF1 (2,(f | Z),z0))
;
(SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y
then A10:
y in dom (reproj (2,z0))
by FUNCT_1:11;
A11:
(reproj (2,z0)) . y in dom (f | Z)
by A9, FUNCT_1:11;
(SVF1 (2,(f | Z),z0)) . y =
(f | Z) . ((reproj (2,z0)) . y)
by A9, FUNCT_1:12
.=
f . ((reproj (2,z0)) . y)
by A11, FUNCT_1:47
.=
(SVF1 (2,f,z0)) . y
by A10, FUNCT_1:13
;
hence
(SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y
;
verum
end;
A12:
y0 in N
by RCOMP_1:16;
assume A13:
y in N
;
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
then (L . (y - y0)) + (R . (y - y0)) =
((SVF1 (2,(f | Z),z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0)
by A6
.=
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,(f | Z),z0)) . y0)
by A4, A13, A8
.=
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0)
by A4, A8, A12
;
hence
((SVF1 (2,f,z0)) . y) - ((SVF1 (2,f,z0)) . y0) = (L . (y - y0)) + (R . (y - y0))
;
verum
end;
for y being Real st y in dom (SVF1 (2,(f | Z),z0)) holds
y in dom (SVF1 (2,f,z0))
proof
let y be
Real;
( y in dom (SVF1 (2,(f | Z),z0)) implies y in dom (SVF1 (2,f,z0)) )
dom (f | Z) = (dom f) /\ Z
by RELAT_1:61;
then A14:
dom (f | Z) c= dom f
by XBOOLE_1:17;
assume
y in dom (SVF1 (2,(f | Z),z0))
;
y in dom (SVF1 (2,f,z0))
then
(
y in dom (reproj (2,z0)) &
(reproj (2,z0)) . y in dom (f | Z) )
by FUNCT_1:11;
hence
y in dom (SVF1 (2,f,z0))
by A14, FUNCT_1:11;
verum
end;
then
for y being object st y in dom (SVF1 (2,(f | Z),z0)) holds
y in dom (SVF1 (2,f,z0))
;
then
dom (SVF1 (2,(f | Z),z0)) c= dom (SVF1 (2,f,z0))
;
then
N c= dom (SVF1 (2,f,z0))
by A4;
hence
f is_partial_differentiable_in z0,2
by A2, A7, Th10; verum