let F be RealNormSpace; for Z being open Subset of REAL
for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
let Z be open Subset of REAL; for f being PartFunc of REAL, the carrier of F st Z c= dom f & ex r being Point of F st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
let f be PartFunc of REAL, the carrier of F; ( Z c= dom f & ex r being Point of F st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) ) )
set R = REAL --> (0. F);
A1:
dom (REAL --> (0. F)) = REAL
;
then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
reconsider L = REAL --> (0. F) as Function of REAL,F ;
then reconsider L = L as LinearFunc of F by Def2;
assume A4:
Z c= dom f
; ( for r being Point of F holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) ) )
given r being Point of F such that A5:
rng f = {r}
; ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )
hence A14:
f is_differentiable_on Z
by A4, Th10; for x being Real st x in Z holds
(f `| Z) /. x = 0. F
let x0 be Real; ( x0 in Z implies (f `| Z) /. x0 = 0. F )
assume A15:
x0 in Z
; (f `| Z) /. x0 = 0. F
then A16:
f is_differentiable_in x0
by A8;
then
ex N being Neighbourhood of x0 st
( N c= dom f & ex L being LinearFunc of F ex R being RestFunc of F st
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
;
then consider N being Neighbourhood of x0 such that
A17:
N c= dom f
;
A18:
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
dom (f `| Z) = Z
by A14, Def6;
hence (f `| Z) /. x0 =
(f `| Z) . x0
by A15, PARTFUN1:def 6
.=
diff (f,x0)
by A14, A15, Def6
.=
L /. jj
by A16, A17, A18, Def4
.=
0. F
;
verum