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 ; :: 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;

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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc, R being RestFunc 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))

y in dom (SVF1 (2,f,z0))

y in dom (SVF1 (2,f,z0)) ;

then dom (SVF1 (2,(f | Z),z0)) c= dom (SVF1 (2,f,z0)) ;

then N c= dom (SVF1 (2,f,z0)) by A4;

hence f is_partial_differentiable_in z0,2 by A2, A7, Th10; :: thesis: verum

( 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 ; :: 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;

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 LinearFunc ex R being RestFunc 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 LinearFunc ex R being RestFunc 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 LinearFunc, R being RestFunc 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

for y being Real st y in dom (SVF1 (2,(f | Z),z0)) holds
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

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;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

A12:
y0 in N
by RCOMP_1:16;
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:11;

A11: (reproj (2,z0)) . y in dom (f | Z) by A9, FUNCT_1:11;

(SVF1 (2,(f | Z),z0)) . y = (f | Z) . ((reproj (2,z0)) . y) by A9, FUNCT_1:12

.= f . ((reproj (2,z0)) . y) by A11, FUNCT_1:47

.= (SVF1 (2,f,z0)) . y by A10, FUNCT_1:13 ;

hence (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y ; :: thesis: verum

end;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:11;

A11: (reproj (2,z0)) . y in dom (f | Z) by A9, FUNCT_1:11;

(SVF1 (2,(f | Z),z0)) . y = (f | Z) . ((reproj (2,z0)) . y) by A9, FUNCT_1:12

.= f . ((reproj (2,z0)) . y) by A11, FUNCT_1:47

.= (SVF1 (2,f,z0)) . y by A10, FUNCT_1:13 ;

hence (SVF1 (2,(f | Z),z0)) . y = (SVF1 (2,f,z0)) . y ; :: thesis: verum

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

y in dom (SVF1 (2,f,z0))

proof

then
for y being object st y in dom (SVF1 (2,(f | Z),z0)) holds
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:61;

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:11;

hence y in dom (SVF1 (2,f,z0)) by A14, FUNCT_1:11; :: thesis: verum

end;dom (f | Z) = (dom f) /\ Z by RELAT_1:61;

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:11;

hence y in dom (SVF1 (2,f,z0)) by A14, FUNCT_1:11; :: thesis: verum

y in dom (SVF1 (2,f,z0)) ;

then dom (SVF1 (2,(f | Z),z0)) c= dom (SVF1 (2,f,z0)) ;

then N c= dom (SVF1 (2,f,z0)) by A4;

hence f is_partial_differentiable_in z0,2 by A2, A7, Th10; :: thesis: verum