let F be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ;

now :: thesis: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )

let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F )

now :: thesis: for n being Nat holds ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F

let n be Nat; :: thesis: ((h ") (#) ((REAL --> (0. F)) /* h)) . n = 0. F
A2: rng h c= dom (REAL --> (0. F)) ;
A3: n in NAT by ORDINAL1:def 12;
thus ((h ") (#) ((REAL --> (0. F)) /* h)) . n = ((h ") . n) * (((REAL --> (0. F)) /* h) . n) by NDIFF_1:def 2
.= ((h ") . n) * ((REAL --> (0. F)) /. (h . n)) by A3, A2, FUNCT_2:108
.= 0. F by RLVECT_1:10 ; :: thesis: verum

end;

then ( (h ") (#) ((REAL --> (0. F)) /* h) is constant & ((h ") (#) ((REAL --> (0. F)) /* h)) . 0 = 0. F ) by VALUED_0:def 18;
hence ( (h ") (#) ((REAL --> (0. F)) /* h) is convergent & lim ((h ") (#) ((REAL --> (0. F)) /* h)) = 0. F ) by NDIFF_1:18; :: thesis: verum

end;

then reconsider R = REAL --> (0. F) as RestFunc of F by Def1;
reconsider L = REAL --> (0. F) as Function of REAL,F ;

now :: thesis: for p being Real holds L /. p = p * (0. F)

let p be Real; :: thesis: L /. p = p * (0. F)
reconsider pp = p as Element of REAL by XREAL_0:def 1;
thus L /. p = L /. pp
.= 0. F
.= p * (0. F) by RLVECT_1:10 ; :: thesis: verum

end;

then reconsider L = L as LinearFunc of F by Def2;
assume A4: Z c= dom f ; :: thesis: ( 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} ; :: thesis: ( f is_differentiable_on Z & ( for x being Real st x in Z holds
(f `| Z) /. x = 0. F ) )

A6: now :: thesis: for x0 being Real st x0 in dom f holds
f /. x0 = r

let x0 be Real; :: thesis: ( x0 in dom f implies f /. x0 = r )
assume A7: x0 in dom f ; :: thesis: f /. x0 = r
then f /. x0 = f . x0 by PARTFUN1:def 6;
then f /. x0 in {r} by A5, A7, FUNCT_1:def 3;
hence f /. x0 = r by TARSKI:def 1; :: thesis: verum

end;

A8: now :: thesis: for x0 being Real st x0 in Z holds
f is_differentiable_in x0

let x0 be Real; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A9: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A10: N c= Z by RCOMP_1:18;
A11: N c= dom f by A4, A10;
for x being Real st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))

proof

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A12: x - x0 in REAL by XREAL_0:def 1;
then A13: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7, A12 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A11
.= r - r by A4, A6, A9
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7, A12
.= L /. (x - x0) by A1, PARTFUN1:def 6, A12
.= (L /. (x - x0)) + (R /. (x - x0)) by A13, RLVECT_1:4 ;
:: thesis: verum

end;

hence f is_differentiable_in x0 by A11; :: thesis: verum

end;

hence A14: f is_differentiable_on Z by A4, Th10; :: thesis: for x being Real st x in Z holds
(f `| Z) /. x = 0. F
let x0 be Real; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. F )
assume A15: x0 in Z ; :: thesis: (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))

proof

let x be Real; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A19: x - x0 in REAL by XREAL_0:def 1;
then A20: R /. (x - x0) = R . (x - x0) by A1, PARTFUN1:def 6
.= 0. F by FUNCOP_1:7, A19 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A6, A17
.= r - r by A4, A6, A15
.= 0. F by RLVECT_1:15
.= L . (x - x0) by FUNCOP_1:7, A19
.= L /. (x - x0) by A1, PARTFUN1:def 6, A19
.= (L /. (x - x0)) + (R /. (x - x0)) by A20, RLVECT_1:4 ;
:: thesis: verum

end;

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