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

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

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

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

reconsider R = the carrier of S --> (0. T) as PartFunc of S,T ;
set L = 0. ;
assume that
A2: Z c= dom f and
A3: 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) = NORMSTR(# (),(Zero_ ((),())),(Add_ ((),())),(Mult_ ((),())),() #) by LOPBAN_1:def 14;
then reconsider L = 0. as Element of BoundedLinearOperators (S,T) ;
A4: dom R = the carrier of S ;
now :: thesis: for h being 0. S -convergent sequence of S st h is non-zero holds
( () (#) (R /* h) is convergent & lim (() (#) (R /* h)) = 0. T )
let h be 0. S -convergent sequence of S; :: thesis: ( h is non-zero implies ( () (#) (R /* h) is convergent & lim (() (#) (R /* h)) = 0. T ) )
assume h is non-zero ; :: thesis: ( () (#) (R /* h) is convergent & lim (() (#) (R /* h)) = 0. T )
A5: now :: thesis: for n being Nat holds (() (#) (R /* h)) . n = 0. T
let n be Nat; :: thesis: (() (#) (R /* h)) . n = 0. T
A6: R /. (h . n) = R . (h . n) by
.= 0. T ;
A7: rng h c= dom R ;
A8: n in NAT by ORDINAL1:def 12;
thus (() (#) (R /* h)) . n = (() . n) * ((R /* h) . n) by Def2
.= (() . n) * (R /. (h . n)) by
.= 0. T by ; :: thesis: verum
end;
then A9: (||.h.|| ") (#) (R /* h) is constant by VALUED_0:def 18;
hence (||.h.|| ") (#) (R /* h) is convergent by Th18; :: thesis: lim (() (#) (R /* h)) = 0. T
((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A5;
hence lim (() (#) (R /* h)) = 0. T by ; :: thesis: verum
end;
then reconsider R = R as RestFunc of S,T by Def5;
consider r being Point of T such that
A10: for x being Point of S st x in Z /\ (dom f) holds
f . x = r by ;
A11: now :: thesis: for x being Point of S st x in Z /\ (dom f) holds
f /. x = r
let x be Point of S; :: thesis: ( x in Z /\ (dom f) implies f /. x = r )
assume A12: 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
.= r by ;
:: thesis: verum
end;
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:
then consider N being Neighbourhood of x0 such that
A16: N c= Z by ;
A17: N c= dom f by ;
A18: x0 in Z /\ (dom f) by ;
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)) )
A19: R /. (x - x0) = R . (x - x0) by
.= 0. T ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by ;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11
.= r - r by
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by ;
:: thesis: verum
end;
hence f is_differentiable_in x0 by A17; :: thesis: verum
end;
hence A20: 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.

let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. )
assume A21: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0.
then consider N being Neighbourhood of x0 such that
A22: N c= Z by ;
A23: N c= dom f by ;
A24: x0 in Z /\ (dom f) by ;
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
.= 0. T ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by ;
hence (f /. x) - (f /. x0) = r - (f /. x0) by A11
.= r - r by
.= 0. T by RLVECT_1:15
.= (0. T) + (0. T) by RLVECT_1:4
.= (L . (x - x0)) + (R /. (x - x0)) by ;
:: thesis: verum
end;
A27: f is_differentiable_in x0 by ;
thus (f `| Z) /. x0 = diff (f,x0) by
.= 0. by ; :: thesis: verum