let Z be Subset of (REAL 2); :: thesis: for f being PartFunc of (REAL 2),REAL st f is_partial_differentiable`1_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,1 ) )
let f be PartFunc of (REAL 2),REAL; :: thesis: ( f is_partial_differentiable`1_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,1 ) ) )
set g = f | Z;
assume A1: f is_partial_differentiable`1_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,1 ) )
hence Z c= dom f ; :: thesis: for z being Element of REAL 2 st z in Z holds
f is_partial_differentiable_in z,1
let z0 be Element of REAL 2; :: thesis: ( z0 in Z implies f is_partial_differentiable_in z0,1 )
assume z0 in Z ; :: thesis: f is_partial_differentiable_in z0,1
then f | Z is_partial_differentiable_in z0,1 by A1;
then consider x0, y0 being Real such that
A2: z0 = <*x0,y0*> and
A3: ex N being Neighbourhood of x0 st
( N c= dom (SVF1 (1,(f | Z),z0)) & ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ) by Th9;
consider N being Neighbourhood of x0 such that
A4: N c= dom (SVF1 (1,(f | Z),z0)) and
A5: ex L being LinearFunc ex R being RestFunc st
for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A3;
consider L being LinearFunc, R being RestFunc such that
A6: for x being Real st x in N holds
((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
A7: for x being Real st x in N holds
((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0))

proof

let x be Real; :: thesis: ( x in N implies ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) )
A8: for x being Real st x in dom (SVF1 (1,(f | Z),z0)) holds
(SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x

proof

let x be Real; :: thesis: ( x in dom (SVF1 (1,(f | Z),z0)) implies (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x )
assume A9: x in dom (SVF1 (1,(f | Z),z0)) ; :: thesis: (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x
then A10: x in dom (reproj (1,z0)) by FUNCT_1:11;
A11: (reproj (1,z0)) . x in dom (f | Z) by A9, FUNCT_1:11;
(SVF1 (1,(f | Z),z0)) . x = (f | Z) . ((reproj (1,z0)) . x) by A9, FUNCT_1:12
.= f . ((reproj (1,z0)) . x) by A11, FUNCT_1:47
.= (SVF1 (1,f,z0)) . x by A10, FUNCT_1:13 ;
hence (SVF1 (1,(f | Z),z0)) . x = (SVF1 (1,f,z0)) . x ; :: thesis: verum

end;

A12: x0 in N by RCOMP_1:16;
assume A13: x in N ; :: thesis: ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0))
then (L . (x - x0)) + (R . (x - x0)) = ((SVF1 (1,(f | Z),z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) by A6
.= ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,(f | Z),z0)) . x0) by A4, A13, A8
.= ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) by A4, A8, A12 ;
hence ((SVF1 (1,f,z0)) . x) - ((SVF1 (1,f,z0)) . x0) = (L . (x - x0)) + (R . (x - x0)) ; :: thesis: verum

end;

for x being Real st x in dom (SVF1 (1,(f | Z),z0)) holds
x in dom (SVF1 (1,f,z0))

proof

let x be Real; :: thesis: ( x in dom (SVF1 (1,(f | Z),z0)) implies x in dom (SVF1 (1,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 x in dom (SVF1 (1,(f | Z),z0)) ; :: thesis: x in dom (SVF1 (1,f,z0))
then ( x in dom (reproj (1,z0)) & (reproj (1,z0)) . x in dom (f | Z) ) by FUNCT_1:11;
hence x in dom (SVF1 (1,f,z0)) by A14, FUNCT_1:11; :: thesis: verum

end;

then for x being object st x in dom (SVF1 (1,(f | Z),z0)) holds
x in dom (SVF1 (1,f,z0)) ;
then dom (SVF1 (1,(f | Z),z0)) c= dom (SVF1 (1,f,z0)) ;
then N c= dom (SVF1 (1,f,z0)) by A4;
hence f is_partial_differentiable_in z0,1 by A2, A7, Th9; :: thesis: verum