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

proof

let z be Real; :: thesis: ( z in dom (SVF1 3,(f | D),u0) implies z in dom (SVF1 3,f,u0) )
assume z in dom (SVF1 3,(f | D),u0) ; :: thesis: z in dom (SVF1 3,f,u0)
then A7: ( z in dom (reproj 3,u0) & (reproj 3,u0) . z in dom (f | D) ) by 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 z in dom (SVF1 3,f,u0) by A7, FUNCT_1:21; :: thesis: verum

end;

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

proof

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

proof

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

end;

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

end;

hence f is_partial_differentiable_in u0,3 by A3, A8, BXXLXSDef11ForZ; :: thesis: verum