let S be non trivial RealNormSpace; :: thesis:
let f be PartFunc of S,S; :: thesis:
let Z be Subset of S; :: thesis:
assume A1: Z is open ; :: thesis:
assume that
A2: Z c= dom f and
A3: f | Z = id Z ; :: thesis:
A4: R_NormSpace_of_BoundedLinearOperators S,S = NORMSTR(# (BoundedLinearOperators S,S),(Zero_ (BoundedLinearOperators S,S),(R_VectorSpace_of_LinearOperators S,S)),(Add_ (BoundedLinearOperators S,S),(R_VectorSpace_of_LinearOperators S,S)),(Mult_ (BoundedLinearOperators S,S),(R_VectorSpace_of_LinearOperators S,S)),(BoundedLinearOperatorsNorm S,S) #) by LOPBAN_1:def 15;
set L = id the carrier of S;
id the carrier of S is bounded LinearOperator of S,S by LOPBAN_2:3;
then reconsider L = id the carrier of S as Point of (R_NormSpace_of_BoundedLinearOperators S,S) by A4, LOPBAN_1:def 10;
reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;
A5: dom R = the carrier of S by FUNCOP_1:19;

now

let h be convergent_to_0 sequence of S; :: thesis:

A7: now

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

end;

then A10: (||.h.|| " ) (#) (R /* h) is constant by VALUED_0:def 18;
hence (||.h.|| " ) (#) (R /* h) is convergent by Th21; :: thesis:
((||.h.|| " ) (#) (R /* h)) . 0 = 0. S by A7;
hence lim ((||.h.|| " ) (#) (R /* h)) = 0. S by A10, Th21; :: thesis:

end;

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

A11: now

let x be Point of S; :: thesis:
assume A12: x in Z ; :: thesis:
then (f | Z) . x = x by A3, FUNCT_1:35;
then f . x = x by A12, FUNCT_1:72;
hence f /. x = x by A2, A12, PARTFUN1:def 8; :: thesis:

end;

A13: now

let x0 be Point of S; :: thesis:
assume A14: x0 in Z ; :: thesis:
then consider N being Neighbourhood of x0 such that
A15: N c= Z by A1, Th2;
A16: N c= dom f by A2, A15, 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:
assume A17: x in N ; :: thesis:
A18: R /. (x - x0) = R . (x - x0) by A5, PARTFUN1:def 8
.= 0. S by FUNCOP_1:13 ;
thus (f /. x) - (f /. x0) = x - (f /. x0) by A11, A15, A17
.= x - x0 by A11, A14
.= L . (x - x0) by FUNCT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A18, RLVECT_1:10 ; :: thesis:

end;

hence f is_differentiable_in x0 by A16, Def6; :: thesis:

end;

hence A19: f is_differentiable_on Z by A1, A2, Th36; :: thesis:
let x0 be Point of S; :: thesis:
assume A20: x0 in Z ; :: thesis:
then A21: f is_differentiable_in x0 by A13;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being Point of (R_NormSpace_of_BoundedLinearOperators S,S) ex R being REST of S,S st
for x being Point of S st x in N holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) ) by Def6;
then consider N being Neighbourhood of x0 such that
A22: N c= dom f ;
consider N1 being Neighbourhood of x0 such that
A23: N1 c= Z by A1, A20, Th2;
consider N2 being Neighbourhood of x0 such that
A24: ( N2 c= N1 & N2 c= N ) by Th1;
A25: N2 c= dom f by A22, A24, XBOOLE_1:1;
A26: for x being Point of S st x in N2 holds
(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

let x be Point of S; :: thesis:
A27: R /. (x - x0) = R . (x - x0) by A5, PARTFUN1:def 8
.= 0. S by FUNCOP_1:13 ;
assume x in N2 ; :: thesis:
then x in N1 by A24;
hence (f /. x) - (f /. x0) = x - (f /. x0) by A11, A23
.= x - x0 by A11, A20
.= L . (x - x0) by FUNCT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A27, RLVECT_1:10 ;
:: thesis:

end;

thus (f `| Z) /. x0 = diff f,x0 by A19, A20, Def9
.= id the carrier of S by A21, A25, A26, Def7 ; :: thesis: