let S be non trivial RealNormSpace; :: thesis:
let f be PartFunc of S,S; :: thesis:
let r be Real; :: thesis:
let p be Point of S; :: thesis:
let Z be Subset of S; :: thesis:
assume A1: Z is open ; :: thesis:
assume A2: ( Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) ) ; :: thesis:
A3: 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;
then reconsider II = FuncUnit S as Point of (R_NormSpace_of_BoundedLinearOperators S,S) ;
set L = r * II;
reconsider L = r * II as Point of (R_NormSpace_of_BoundedLinearOperators S,S) ;
A4: L = r * (FuncUnit S) by A3, LOPBAN_2:def 3;
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 x0 be Point of S; :: thesis:
assume A12: x0 in Z ; :: thesis:
then consider N being Neighbourhood of x0 such that
A13: N c= Z by A1, Th2;
A14: N c= dom f by A2, A13, 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 A15: x in N ; :: thesis:
A16: R /. (x - x0) = R . (x - x0) by A5, PARTFUN1:def 8
.= 0. S by FUNCOP_1:13 ;
x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:34;
then A17: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def 5
.= L . (x - x0) by LOPBAN_1:42 ;
thus (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A2, A13, A15
.= ((r * x) + p) - ((r * x0) + p) by A2, A12
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def 6
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:41
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def 6
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:28
.= (r * x) - (r * x0) by RLVECT_1:10
.= r * (x - x0) by RLVECT_1:48
.= (L . (x - x0)) + (R /. (x - x0)) by A16, A17, RLVECT_1:10 ; :: thesis:

end;

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

end;

hence A18: f is_differentiable_on Z by A1, A2, Th36; :: thesis:
let x0 be Point of S; :: thesis:
assume A19: x0 in Z ; :: thesis:
then A20: f is_differentiable_in x0 by A11;
consider N being Neighbourhood of x0 such that
A21: N c= Z by A1, A19, Th2;
A22: N c= dom f by A2, A21, XBOOLE_1:1;
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:
assume A24: x in N ; :: thesis:
A25: R /. (x - x0) = R . (x - x0) by A5, PARTFUN1:def 8
.= 0. S by FUNCOP_1:13 ;
x - x0 = (id the carrier of S) . (x - x0) by FUNCT_1:34;
then A26: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def 5
.= L . (x - x0) by LOPBAN_1:42 ;
thus (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A2, A21, A24
.= ((r * x) + p) - ((r * x0) + p) by A2, A19
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def 6
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:41
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def 6
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:28
.= (r * x) - (r * x0) by RLVECT_1:10
.= r * (x - x0) by RLVECT_1:48
.= (L . (x - x0)) + (R /. (x - x0)) by A25, A26, RLVECT_1:10 ; :: thesis:

end;

thus (f `| Z) /. x0 = diff f,x0 by A18, A19, Def9
.= r * (FuncUnit S) by A4, A20, A22, A23, Def7 ; :: thesis: