let S, T be 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 RestFunc 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 RestFunc 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 RestFunc 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 RestFunc 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 RestFunc 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 RestFunc 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 RestFunc 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

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 14;
then reconsider L = diff (f,x0) as Element of BoundedLinearOperators (S,T) ;
consider R being RestFunc 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)) ) )
(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:15;
then 0. T = (L . (0. S)) + (R /. (x0 - x0)) by RLVECT_1:15;
then A4: 0. T = (L . (0. S)) + (R /. (0. S)) by RLVECT_1:15;
L . (0. S) = (modetrans (L,S,T)) . (0. S) by LOPBAN_1:def 11
.= (modetrans (L,S,T)) . (0 * (0. S)) by RLVECT_1:10
.= 0 * ((modetrans (L,S,T)) . (0. S)) by LOPBAN_1:def 5
.= 0. T by RLVECT_1:10 ;
hence A5: R /. (0. S) = 0. T by A4, RLVECT_1:4; :: 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: now :: thesis: for s1 being sequence of S st rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Nat holds s1 . n <> 0. S ) holds
( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) )

let s1 be sequence of S; :: thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0. S & ( for n being Nat holds s1 . n <> 0. S ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) )
assume that
rng s1 c= dom R and
A7: ( s1 is convergent & lim s1 = 0. S ) and
A8: for n being Nat holds s1 . n <> 0. S ; :: thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) )
A9: s1 is 0. S -convergent sequence of S by A7, Def4;
s1 is non-zero by A8, Th7;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. (0. S) ) by A5, A9, Th24; :: thesis: verum

end;

R is total by Def5;
then dom R = the carrier of S by PARTFUN1:def 2;
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, A6, Th27; :: thesis: verum

end;

hence ( N c= dom f & ex R being RestFunc 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