let S be RealNormSpace; :: thesis: for f being PartFunc of S,S

for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

set L = id the carrier of S;

( 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)) #) & id the carrier of S is Lipschitzian LinearOperator of S,S ) by LOPBAN_1:def 14, LOPBAN_2:3;

then reconsider L = id the carrier of S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) by LOPBAN_1:def 9;

let f be PartFunc of S,S; :: thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

let Z be Subset of S; :: thesis: ( Z is open & Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) ) )

assume A1: Z is open ; :: thesis: ( not Z c= dom f or not f | Z = id Z or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) ) )

reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;

A2: dom R = the carrier of S ;

assume that

A8: Z c= dom f and

A9: f | Z = id Z ; :: thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

(f `| Z) /. x = id the carrier of S

let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = id the carrier of S )

assume A18: x0 in Z ; :: thesis: (f `| Z) /. x0 = id the carrier of S

then consider N1 being Neighbourhood of x0 such that

A19: N1 c= Z by A1, Th2;

A20: f is_differentiable_in x0 by A12, A18;

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 RestFunc 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)) ) ;

then consider N being Neighbourhood of x0 such that

A21: N c= dom f ;

consider N2 being Neighbourhood of x0 such that

A22: N2 c= N1 and

A23: N2 c= N by Th1;

A24: N2 c= dom f by A21, A23;

A25: for x being Point of S st x in N2 holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

.= id the carrier of S by A20, A24, A25, Def7 ; :: thesis: verum

for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

set L = id the carrier of S;

( 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)) #) & id the carrier of S is Lipschitzian LinearOperator of S,S ) by LOPBAN_1:def 14, LOPBAN_2:3;

then reconsider L = id the carrier of S as Point of (R_NormSpace_of_BoundedLinearOperators (S,S)) by LOPBAN_1:def 9;

let f be PartFunc of S,S; :: thesis: for Z being Subset of S st Z is open & Z c= dom f & f | Z = id Z holds

( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

let Z be Subset of S; :: thesis: ( Z is open & Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) ) )

assume A1: Z is open ; :: thesis: ( not Z c= dom f or not f | Z = id Z or ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) ) )

reconsider R = the carrier of S --> (0. S) as PartFunc of S,S ;

A2: 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 )

then reconsider R = R as RestFunc of S,S by Def5;( (||.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 )

hence (||.h.|| ") (#) (R /* h) is convergent by Th18; :: thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S

((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A3;

hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A7, Th18; :: thesis: verum

end;assume h is non-zero ; :: thesis: ( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. S )

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

then A7:
(||.h.|| ") (#) (R /* h) is constant
by VALUED_0:def 18;let n be Nat; :: thesis: ((||.h.|| ") (#) (R /* h)) . n = 0. S

A4: R /. (h . n) = R . (h . n) by A2, PARTFUN1:def 6

.= 0. S ;

A5: rng h c= dom R ;

A6: 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 A6, A5, FUNCT_2:109

.= 0. S by A4, RLVECT_1:10 ; :: thesis: verum

end;A4: R /. (h . n) = R . (h . n) by A2, PARTFUN1:def 6

.= 0. S ;

A5: rng h c= dom R ;

A6: 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 A6, A5, FUNCT_2:109

.= 0. S by A4, RLVECT_1:10 ; :: thesis: verum

hence (||.h.|| ") (#) (R /* h) is convergent by Th18; :: thesis: lim ((||.h.|| ") (#) (R /* h)) = 0. S

((||.h.|| ") (#) (R /* h)) . 0 = 0. S by A3;

hence lim ((||.h.|| ") (#) (R /* h)) = 0. S by A7, Th18; :: thesis: verum

assume that

A8: Z c= dom f and

A9: f | Z = id Z ; :: thesis: ( f is_differentiable_on Z & ( for x being Point of S st x in Z holds

(f `| Z) /. x = id the carrier of S ) )

A10: now :: thesis: for x being Point of S st x in Z holds

f /. x = x

f /. x = x

let x be Point of S; :: thesis: ( x in Z implies f /. x = x )

assume A11: x in Z ; :: thesis: f /. x = x

then (f | Z) . x = x by A9, FUNCT_1:18;

then f . x = x by A11, FUNCT_1:49;

hence f /. x = x by A8, A11, PARTFUN1:def 6; :: thesis: verum

end;assume A11: x in Z ; :: thesis: f /. x = x

then (f | Z) . x = x by A9, FUNCT_1:18;

then f . x = x by A11, FUNCT_1:49;

hence f /. x = x by A8, A11, PARTFUN1:def 6; :: thesis: verum

A12: now :: thesis: for x0 being Point of S st x0 in Z holds

f is_differentiable_in x0

hence A17:
f is_differentiable_on Z
by A1, A8, Th31; :: thesis: for x being Point of S st x 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))

hence f is_differentiable_in x0 by A15; :: thesis: verum

end;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

N c= dom f
by A8, A14;
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 A2, PARTFUN1:def 6

.= 0. S ;

assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A14

.= x - x0 by A10, A13

.= L . (x - x0)

.= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ;

:: thesis: verum

end;A16: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def 6

.= 0. S ;

assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A14

.= x - x0 by A10, A13

.= L . (x - x0)

.= (L . (x - x0)) + (R /. (x - x0)) by A16, RLVECT_1:4 ;

:: thesis: verum

hence f is_differentiable_in x0 by A15; :: thesis: verum

(f `| Z) /. x = id the carrier of S

let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = id the carrier of S )

assume A18: x0 in Z ; :: thesis: (f `| Z) /. x0 = id the carrier of S

then consider N1 being Neighbourhood of x0 such that

A19: N1 c= Z by A1, Th2;

A20: f is_differentiable_in x0 by A12, A18;

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 RestFunc 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)) ) ;

then consider N being Neighbourhood of x0 such that

A21: N c= dom f ;

consider N2 being Neighbourhood of x0 such that

A22: N2 c= N1 and

A23: N2 c= N by Th1;

A24: N2 c= dom f by A21, A23;

A25: for x being Point of S st x in N2 holds

(f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

proof

thus (f `| Z) /. x0 =
diff (f,x0)
by A17, A18, Def9
let x be Point of S; :: thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0)) )

A26: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def 6

.= 0. S ;

assume x in N2 ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

then x in N1 by A22;

hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A19

.= x - x0 by A10, A18

.= L . (x - x0)

.= (L . (x - x0)) + (R /. (x - x0)) by A26, RLVECT_1:4 ;

:: thesis: verum

end;A26: R /. (x - x0) = R . (x - x0) by A2, PARTFUN1:def 6

.= 0. S ;

assume x in N2 ; :: thesis: (f /. x) - (f /. x0) = (L . (x - x0)) + (R /. (x - x0))

then x in N1 by A22;

hence (f /. x) - (f /. x0) = x - (f /. x0) by A10, A19

.= x - x0 by A10, A18

.= L . (x - x0)

.= (L . (x - x0)) + (R /. (x - x0)) by A26, RLVECT_1:4 ;

:: thesis: verum

.= id the carrier of S by A20, A24, A25, Def7 ; :: thesis: verum