let E, F be RealNormSpace; :: thesis: for f being PartFunc of E,F
for Z being Subset of E
for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds
( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )
let f be PartFunc of E,F; :: thesis: for Z being Subset of E
for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds
( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )
let Z be Subset of E; :: thesis: for z being Point of E st Z is open & z in Z & Z c= dom f & f is_differentiable_in z holds
( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )
let z be Point of E; :: thesis: ( Z is open & z in Z & Z c= dom f & f is_differentiable_in z implies ( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) ) )
assume A1: ( Z is open & z in Z & Z c= dom f & f is_differentiable_in z ) ; :: thesis: ( f | Z is_differentiable_in z & diff (f,z) = diff ((f | Z),z) )
then consider N being Neighbourhood of z such that
A2: ( N c= dom f & ex R being RestFunc of E,F st
for x being Point of E st x in N holds
(f /. x) - (f /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z)) ) by NDIFF_1:def 7;
consider r being Real such that
A3: ( r > 0 & Ball (z,r) c= Z ) by A1, NDIFF_8:20;
Ball (z,r) = { y where y is Point of E : ||.(y - z).|| < r } by NDIFF_8:17;
then Z is Neighbourhood of z by A3, NFCONT_1:def 1;
then reconsider NZ = N /\ Z as Neighbourhood of z by NDIFF_5:8;
A4: dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
A5: N /\ Z c= (dom f) /\ Z by A2, XBOOLE_1:26;
consider R being RestFunc of E,F such that
A6: for x being Point of E st x in N holds
(f /. x) - (f /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z)) by A2;
A7: for x being Point of E st x in NZ holds
((f | Z) /. x) - ((f | Z) /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z))

proof

let x be Point of E; :: thesis: ( x in NZ implies ((f | Z) /. x) - ((f | Z) /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z)) )
assume A8: x in NZ ; :: thesis: ((f | Z) /. x) - ((f | Z) /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z))
then A9: ( x in N & x in Z ) by XBOOLE_0:def 4;
then A15: f /. x = f . x by A2, PARTFUN1:def 6
.= (f | Z) . x by A9, FUNCT_1:49
.= (f | Z) /. x by A4, A5, A8, PARTFUN1:def 6 ;
A14: z in NZ by NFCONT_1:4;
f /. z = f . z by A1, PARTFUN1:def 6
.= (f | Z) . z by A1, FUNCT_1:49
.= (f | Z) /. z by A4, A5, A14, PARTFUN1:def 6 ;
hence ((f | Z) /. x) - ((f | Z) /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z)) by A6, A9, A15; :: thesis: verum

end;

hence f | Z is_differentiable_in z by A2, A4, NDIFF_1:def 6, XBOOLE_1:26; :: thesis: diff (f,z) = diff ((f | Z),z)
hence diff (f,z) = diff ((f | Z),z) by A4, A5, A7, NDIFF_1:def 7; :: thesis: verum