let Z be Subset of (REAL 2); :: thesis: 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 ; :: thesis: ( 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 ; :: thesis: ( 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 by Def3; :: thesis: 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; :: thesis: ( z0 in Z implies f is_partial_differentiable_in z0,2 )
assume z0 in Z ; :: thesis: f is_partial_differentiable_in z0,2
then f | Z is_partial_differentiable_in z0,2 by A1, Def3;
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 LINEAR ex R being REST 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 LINEAR ex R being REST 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 LINEAR, R being REST 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; :: thesis: ( 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; :: thesis: ( 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) ; :: thesis: (SVF1 2,(f | Z),z0) . y = (SVF1 2,f,z0) . y
then A10: y in dom (reproj 2,z0) by FUNCT_1:21;
A11: (reproj 2,z0) . y in dom (f | Z) by A9, FUNCT_1:21;
(SVF1 2,(f | Z),z0) . y = (f | Z) . ((reproj 2,z0) . y) by A9, FUNCT_1:22
.= f . ((reproj 2,z0) . y) by A11, FUNCT_1:70
.= (SVF1 2,f,z0) . y by A10, FUNCT_1:23 ;
hence (SVF1 2,(f | Z),z0) . y = (SVF1 2,f,z0) . y ; :: thesis: verum

end;

A12: y0 in N by RCOMP_1:37;
assume A13: y in N ; :: thesis: ((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)) ; :: thesis: 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; :: thesis: ( 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:90;
then A14: dom (f | Z) c= dom f by XBOOLE_1:17;
assume y in dom (SVF1 2,(f | Z),z0) ; :: thesis: 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:21;
hence y in dom (SVF1 2,f,z0) by A14, FUNCT_1:21; :: thesis: verum

end;

then for y being set 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) by TARSKI:def 3;
then N c= dom (SVF1 2,f,z0) by A4, XBOOLE_1:1;
hence f is_partial_differentiable_in z0,2 by A2, A7, Th10; :: thesis: verum