let D be set ; :: thesis: for f being PartFunc of (REAL 3),REAL st f is_partial_differentiable`2_on D holds
( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )
let f be PartFunc of (REAL 3),REAL ; :: thesis: ( f is_partial_differentiable`2_on D implies ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) ) )
assume A1: f is_partial_differentiable`2_on D ; :: thesis: ( D c= dom f & ( for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2 ) )
hence D c= dom f by Def17; :: thesis: for u being Element of REAL 3 st u in D holds
f is_partial_differentiable_in u,2
set g = f | D;
let u0 be Element of REAL 3; :: thesis: ( u0 in D implies f is_partial_differentiable_in u0,2 )
assume u0 in D ; :: thesis: f is_partial_differentiable_in u0,2
then A2: f | D is_partial_differentiable_in u0,2 by A1, Def17;
consider x0, y0, z0 being Real such that
A3: ( u0 = <*x0,y0,z0*> & ex N being Neighbourhood of y0 st
( N c= dom (SVF1 2,(f | D),u0) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF1 2,(f | D),u0) . y) - ((SVF1 2,(f | D),u0) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A2, BXXLXSDef11;
consider N being Neighbourhood of y0 such that
A4: ( N c= dom (SVF1 2,(f | D),u0) & ex L being LINEAR ex R being REST st
for y being Real st y in N holds
((SVF1 2,(f | D),u0) . y) - ((SVF1 2,(f | D),u0) . y0) = (L . (y - y0)) + (R . (y - y0)) ) by A3;
for y being Real st y in dom (SVF1 2,(f | D),u0) holds
y in dom (SVF1 2,f,u0)

proof

let y be Real; :: thesis: ( y in dom (SVF1 2,(f | D),u0) implies y in dom (SVF1 2,f,u0) )
assume A6: y in dom (SVF1 2,(f | D),u0) ; :: thesis: y in dom (SVF1 2,f,u0)
A7: ( y in dom (reproj 2,u0) & (reproj 2,u0) . y in dom (f | D) ) by A6, FUNCT_1:21;
dom (f | D) = (dom f) /\ D by RELAT_1:90;
then dom (f | D) c= dom f by XBOOLE_1:17;
hence y in dom (SVF1 2,f,u0) by A7, FUNCT_1:21; :: thesis: verum

end;

then for y being set st y in dom (SVF1 2,(f | D),u0) holds
y in dom (SVF1 2,f,u0) ;
then dom (SVF1 2,(f | D),u0) c= dom (SVF1 2,f,u0) by TARSKI:def 3;
then A8: N c= dom (SVF1 2,f,u0) by A4, XBOOLE_1:1;
consider L being LINEAR, R being REST such that
A9: for y being Real st y in N holds
((SVF1 2,(f | D),u0) . y) - ((SVF1 2,(f | D),u0) . y0) = (L . (y - y0)) + (R . (y - y0)) by A4;
for y being Real st y in N holds
((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0))

proof

let y be Real; :: thesis: ( y in N implies ((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) )
assume A10: y in N ; :: thesis: ((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0))
A12: for y being Real st y in dom (SVF1 2,(f | D),u0) holds
(SVF1 2,(f | D),u0) . y = (SVF1 2,f,u0) . y

proof

let y be Real; :: thesis: ( y in dom (SVF1 2,(f | D),u0) implies (SVF1 2,(f | D),u0) . y = (SVF1 2,f,u0) . y )
assume A13: y in dom (SVF1 2,(f | D),u0) ; :: thesis: (SVF1 2,(f | D),u0) . y = (SVF1 2,f,u0) . y
A14: ( y in dom (reproj 2,u0) & (reproj 2,u0) . y in dom (f | D) ) by A13, FUNCT_1:21;
(SVF1 2,(f | D),u0) . y = (f | D) . ((reproj 2,u0) . y) by A13, FUNCT_1:22
.= f . ((reproj 2,u0) . y) by A14, FUNCT_1:70
.= (SVF1 2,f,u0) . y by A14, FUNCT_1:23 ;
hence (SVF1 2,(f | D),u0) . y = (SVF1 2,f,u0) . y ; :: thesis: verum

end;

A16: y0 in N by RCOMP_1:37;
(L . (y - y0)) + (R . (y - y0)) = ((SVF1 2,(f | D),u0) . y) - ((SVF1 2,(f | D),u0) . y0) by A9, A10
.= ((SVF1 2,f,u0) . y) - ((SVF1 2,(f | D),u0) . y0) by A4, A10, A12
.= ((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) by A4, A12, A16 ;
hence ((SVF1 2,f,u0) . y) - ((SVF1 2,f,u0) . y0) = (L . (y - y0)) + (R . (y - y0)) ; :: thesis: verum

end;

hence f is_partial_differentiable_in u0,2 by A3, A8, BXXLXSDef11; :: thesis: verum