let E, F be RealNormSpace; 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; 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; 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; ( 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 )
; ( 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;
( x in NZ implies ((f | Z) /. x) - ((f | Z) /. z) = ((diff (f,z)) . (x - z)) + (R /. (x - z)) )
assume A8:
x in NZ
;
((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;
verum
end;
hence
f | Z is_differentiable_in z
by A2, A4, NDIFF_1:def 6, XBOOLE_1:26; diff (f,z) = diff ((f | Z),z)
hence
diff (f,z) = diff ((f | Z),z)
by A4, A5, A7, NDIFF_1:def 7; verum