let S, T be RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let f be PartFunc of S,T; :: thesis: for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
let Z be Subset of S; :: thesis: ( Z is open & Z c= dom f & ex r being Point of T st rng f = {r} implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
assume that
A1: Z is open and
A2: Z c= dom f ; :: thesis: ( for r being Point of T holds not rng f = {r} or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T));
given r being Point of T such that A3: rng f = {r} ; :: thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )
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 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ;
A4: dom R = the carrier of S ;

A5: now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T ) )
assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

A6: now :: thesis: for n being Nat holds ((||.h.|| ") (#) (R /* h)) . n = 0. T

let n be Nat; :: thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. T
A7: R /. (h . n) = R . (h . n) by A4, PARTFUN1:def 6
.= 0. T ;
A8: rng h c= dom R ;
A9: n in NAT by ORDINAL1:def 12;
thus ((||.h.|| ") (#) (R /* h)) . n = ((||.h.|| ") . n) * ((R /* h) . n) by Def2
.= ((||.h.|| ") . n) * (R /. (h . n)) by A9, A8, FUNCT_2:109
.= 0. T by A7, RLVECT_1:10 ; :: thesis: verum

end;

then A10: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def 18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; :: thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. T
((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A6;
hence lim ((||.h.|| ") (#) (R /* h)) = 0. T by A10, Th18; :: thesis: verum

end;

A11: now :: thesis: for x0 being Point of S st x0 in dom f holds
f /. x0 = r

let x0 be Point of S; :: thesis: ( x0 in dom f implies f /. x0 = r )
assume A12: x0 in dom f ; :: thesis: f /. x0 = r
then f . x0 in {r} by A3, FUNCT_1:def 3;
then f /. x0 in {r} by A12, PARTFUN1:def 6;
hence f /. x0 = r by TARSKI:def 1; :: thesis: verum

end;

reconsider R = R as RestFunc of S,T by A5, Def5;
A13: the carrier of S --> (0. T) = L by LOPBAN_1:31;

A14: now :: thesis: for x0 being Point of S st x0 in Z holds
f is_differentiable_in x0

let x0 be Point of S; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A15: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A16: N c= Z by A1, Th2;
A17: N c= dom f by A2, A16;
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Point of S; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A18: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def 6
.= 0. T ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A17
.= r - r by A2, A11, A15
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A18 ;
:: thesis: verum

end;

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

end;

hence A19: f is_differentiable_on Z by A1, A2, Th31; :: thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )
assume A20: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
then A21: f is_differentiable_in x0 by A14;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) ex R being RestFunc of S,T st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) ;
then consider N being Neighbourhood of x0 such that
A22: N c= dom f ;
A23: for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Point of S; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )
A24: R /. (x - x0) = R . (x - x0) by A4, PARTFUN1:def 6
.= 0. T ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11, A22
.= r - r by A2, A11, A20
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by A13, A24 ;
:: thesis: verum

end;

thus (f `| Z) /. x0 = diff (f,x0) by A19, A20, Def9
.= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A21, A22, A23, Def7 ; :: thesis: verum