let T, S be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) )
let f be PartFunc of S,T; :: thesis: for x0 being Point of S st f is_differentiable_in x0 holds
ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) )
let x0 be Point of S; :: thesis: ( f is_differentiable_in x0 implies ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) ) )
assume f is_differentiable_in x0 ; :: thesis: ex N being Neighbourhood of x0 st
( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) )
then consider N being Neighbourhood of x0 such that
A1: N c= dom f and
A2: ex R being REST of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) by Def7;
take N ; :: thesis: ( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) )
ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) )

proof

consider R being REST of S,T such that
A3: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) by A2;
take R ; :: thesis: ( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) )
R_NormSpace_of_BoundedLinearOperators S,T = NORMSTR(# (BoundedLinearOperators S,T),(Zero_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Add_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(Mult_ (BoundedLinearOperators S,T),(R_VectorSpace_of_LinearOperators S,T)),(BoundedLinearOperatorsNorm S,T) #) by LOPBAN_1:def 15;
then reconsider L = diff f,x0 as Element of BoundedLinearOperators S,T ;
A4: L . (0. S) = (modetrans L,S,T) . (0. S) by LOPBAN_1:def 12
.= (modetrans L,S,T) . (0 * (0. S)) by RLVECT_1:23
.= 0 * ((modetrans L,S,T) . (0. S)) by LOPBAN_1:def 6
.= 0. T by RLVECT_1:23 ;
(f /. x0) - (f /. x0) = (L . (x0 - x0)) + (R /. (x0 - x0)) by A3, NFCONT_1:4;
then 0. T = (L . (x0 - x0)) + (R /. (x0 - x0)) by RLVECT_1:28;
then 0. T = (L . (0. S)) + (R /. (x0 - x0)) by RLVECT_1:28;
then 0. T = (L . (0. S)) + (R /. (0. S)) by RLVECT_1:28;
hence A5: R /. (0. S) = 0. T by A4, RLVECT_1:10; :: thesis: ( R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) )
A6: ( R is total & ( for h being convergent_to_0 sequence of S holds
( (||.h.|| " ) (#) (R /* h) is convergent & lim ((||.h.|| " ) (#) (R /* h)) = 0. T ) ) ) by Def5;

A7: now

let s1 be sequence of S; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Element of NAT holds s1 . n <> 0. S ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) )
assume A8: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Element of NAT holds s1 . n <> 0. S ) ) ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) )
then s1 is non-zero by Th7;
then s1 is convergent_to_0 sequence of S by A8, Def4;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) by A5, Th27; :: thesis: verum

end;

dom R = the carrier of S by A6, PARTFUN1:def 4;
hence ( R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) by A3, A7, Th32; :: thesis: verum

end;

hence ( N c= dom f & ex R being REST of S,T st
( R /. (0. S) = 0. T & R is_continuous_in 0. S & ( for x being Point of S st x in N holds
(f /. x) - (f /. x0) = ((diff f,x0) . (x - x0)) + (R /. (x - x0)) ) ) ) by A1; :: thesis: verum