let S, T be non trivial RealNormSpace; :: thesis: for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & f | Z is constant 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 & f | Z is constant 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 & f | Z is constant 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 A1: Z is open ; :: thesis: ( not Z c= dom f or not f | Z is constant 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) ) ) )
assume A2: ( Z c= dom f & f | Z is constant ) ; :: 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) ) )
then consider r being Point of T such that
A3: for x being Point of S st x in Z /\ (dom f) holds
f . x = r by PARTFUN2:76;

A4: now

let x be Point of S; :: thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A5: x in Z /\ (dom f) ; :: thesis: f /. x = r
Z /\ (dom f) c= dom f by XBOOLE_1:17;
hence f /. x = f . x by A5, PARTFUN1:def 8
.= r by A3, A5 ;
:: thesis: verum

end;

set L = 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 15;
then reconsider L = 0. (R_NormSpace_of_BoundedLinearOperators S,T) as Element of BoundedLinearOperators S,T ;
A6: the carrier of S --> (0. T) = L by LOPBAN_1:37;
reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
A7: dom R = the carrier of S by FUNCOP_1:19;

now

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

A9: now

let n be Nat; :: thesis: ((||.h.|| " ) (#) (R /* h)) . n = 0. T
X: n in NAT by ORDINAL1:def 13;
A10: R /. (h . n) = R . (h . n) by A7, PARTFUN1:def 8
.= 0. T by FUNCOP_1:13 ;
A11: rng h c= dom R by A7;
thus ((||.h.|| " ) (#) (R /* h)) . n = ((||.h.|| " ) . n) * ((R /* h) . n) by Def2, X
.= ((||.h.|| " ) . n) * (R /. (h . n)) by A11, X, FUNCT_2:186
.= 0. T by A10, RLVECT_1:23 ; :: thesis: verum

end;

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

end;

then reconsider R = R as REST of S,T by Def5;

A13: now

let x0 be Point of S; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A14: x0 in Z ; :: thesis: f is_differentiable_in x0
then A15: x0 in Z /\ (dom f) by A2, XBOOLE_0:def 4;
consider N being Neighbourhood of x0 such that
A16: N c= Z by A1, A14, Th2;
A17: N c= dom f by A2, A16, XBOOLE_1:1;
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 A7, PARTFUN1:def 8
.= 0. T by FUNCOP_1:13 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A16, A17, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A4
.= r - r by A4, A15
.= 0. T by RLVECT_1:28
.= (0. T) + (0. T) by RLVECT_1:10
.= (L . (x - x0)) + (R /. (x - x0)) by A6, A18, FUNCOP_1:13 ;
:: thesis: verum

end;

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

end;

hence A19: f is_differentiable_on Z by A1, A2, Th36; :: 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: x0 in Z /\ (dom f) by A2, XBOOLE_0:def 4;
A22: f is_differentiable_in x0 by A13, A20;
consider N being Neighbourhood of x0 such that
A23: N c= Z by A1, A20, Th2;
A24: N c= dom f by A2, A23, XBOOLE_1:1;
A25: 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)) )
A26: R /. (x - x0) = R . (x - x0) by A7, PARTFUN1:def 8
.= 0. T by FUNCOP_1:13 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A23, A24, XBOOLE_0:def 4;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A4
.= r - r by A4, A21
.= 0. T by RLVECT_1:28
.= (0. T) + (0. T) by RLVECT_1:10
.= (L . (x - x0)) + (R /. (x - x0)) by A6, A26, FUNCOP_1:13 ;
:: thesis: verum

end;

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