let S be RealNormSpace; :: thesis: for f being PartFunc of S,S
for r being Real
for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let f be PartFunc of S,S; :: thesis: for r being Real
for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let r be Real; :: thesis: for p being Point of S
for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let p be Point of S; :: thesis: for Z being Subset of S st Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) holds
( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
let Z be Subset of S; :: thesis: ( Z is open & Z c= dom f & ( for x being Point of S st x in Z holds
f /. x = (r * x) + p ) implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) ) )
assume A1: Z is open ; :: thesis: ( not Z c= dom f or ex x being Point of S st
( x in Z & not f /. x = (r * x) + p ) or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) ) )
A2: 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 14;
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)) ;
reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;
assume that
A3: Z c= dom f and
A4: for x being Point of S st x in Z holds
f /. x = (r * x) + p ; :: thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S) ) )
A5: L = r * (FuncUnit S) by A2, LOPBAN_2:def 3;
A6: dom R = the carrier of S ;

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

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. S ) )
assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S )

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

let n be Nat; :: thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S
A8: R /. (h . n) = R . (h . n) by A6, PARTFUN1:def 6
.= 0. S ;
A9: rng h c= dom R ;
A10: 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 A10, A9, FUNCT_2:109
.= 0. S by A8, RLVECT_1:10 ; :: thesis: verum

end;

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

end;

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

A12: 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 A13: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A14: N c= Z by A1, Th2;
A15: 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)) )
A16: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def 6
.= 0. S ;
x - x0 = (id the carrier of S) . (x - x0) ;
then A17: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def 5
.= L . (x - x0) by LOPBAN_1:36 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A14
.= ((r * x) + p) - ((r * x0) + p) by A4, A13
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def 3
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def 3
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15
.= (r * x) - (r * x0) by RLVECT_1:4
.= r * (x - x0) by RLVECT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A16, A17, RLVECT_1:4 ;
:: thesis: verum

end;

N c= dom f by A3, A14;
hence f is_differentiable_in x0 by A15; :: thesis: verum

end;

hence A18: f is_differentiable_on Z by A1, A3, Th31; :: thesis: for x being Point of S st x in Z holds
(f `| Z) /. x = r * (FuncUnit S)
let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = r * (FuncUnit S) )
assume A19: x0 in Z ; :: thesis: (f `| Z) /. x0 = r * (FuncUnit S)
then consider N being Neighbourhood of x0 such that
A20: N c= Z by A1, Th2;
A21: 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)) )
A22: R /. (x - x0) = R . (x - x0) by A6, PARTFUN1:def 6
.= 0. S ;
x - x0 = (id the carrier of S) . (x - x0) ;
then A23: r * (x - x0) = r * ((FuncUnit S) . (x - x0)) by LOPBAN_2:def 5
.= L . (x - x0) by LOPBAN_1:36 ;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((r * x) + p) - (f /. x0) by A4, A20
.= ((r * x) + p) - ((r * x0) + p) by A4, A19
.= (r * x) + (p - ((r * x0) + p)) by RLVECT_1:def 3
.= (r * x) + ((p - (r * x0)) - p) by RLVECT_1:27
.= (r * x) + ((p + (- (r * x0))) - p)
.= (r * x) + ((- (r * x0)) + (p - p)) by RLVECT_1:def 3
.= (r * x) + ((- (r * x0)) + (0. S)) by RLVECT_1:15
.= (r * x) - (r * x0) by RLVECT_1:4
.= r * (x - x0) by RLVECT_1:34
.= (L . (x - x0)) + (R /. (x - x0)) by A22, A23, RLVECT_1:4 ;
:: thesis: verum

end;

A24: N c= dom f by A3, A20;
A25: f is_differentiable_in x0 by A12, A19;
thus (f `| Z) /. x0 = diff (f,x0) by A18, A19, Def9
.= r * (FuncUnit S) by A5, A25, A24, A21, Def7 ; :: thesis: verum