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)) ) )

( 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

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

hence
( N c= dom f & ex R being RestFunc of S,T st
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)) ) )

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;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) )

R is total
by Def5;( 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;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

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

( 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