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

proof

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

end;

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

proof

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

proof

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

end;

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

end;

hence f is_partial_differentiable_in u0,1 by A3, A8, BXXLXSDef10; :: thesis: verum