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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )

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

set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T));

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

R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

then reconsider L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) as Element of BoundedLinearOperators (S,T) ;

A4: dom R = the carrier of S ;

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 A3, PARTFUN2:57;

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))

let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )

assume A21: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))

then consider N being Neighbourhood of x0 such that

A22: N c= Z by A1, Th2;

A23: N c= dom f by A2, A22;

A24: x0 in Z /\ (dom f) by A2, A21, XBOOLE_0:def 4;

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

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

thus (f `| Z) /. x0 = diff (f,x0) by A20, A21, Def9

.= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A27, A23, A25, Def7 ; :: thesis: verum

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )

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. (R_NormSpace_of_BoundedLinearOperators (S,T)) ) ) )

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

set L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T));

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

R_NormSpace_of_BoundedLinearOperators (S,T) = NORMSTR(# (BoundedLinearOperators (S,T)),(Zero_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Add_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(Mult_ ((BoundedLinearOperators (S,T)),(R_VectorSpace_of_LinearOperators (S,T)))),(BoundedLinearOperatorsNorm (S,T)) #) by LOPBAN_1:def 14;

then reconsider L = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) 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

( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

then reconsider R = R as RestFunc of S,T by Def5;( (||.h.|| ") (#) (R /* h) is convergent & lim ((||.h.|| ") (#) (R /* h)) = 0. T )

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

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

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

((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A5;

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

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

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

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

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

.= 0. T ;

A7: rng h c= dom R ;

A8: 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 A8, A7, FUNCT_2:109

.= 0. T by A6, RLVECT_1:10 ; :: thesis: verum

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

.= 0. T ;

A7: rng h c= dom R ;

A8: 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 A8, A7, FUNCT_2:109

.= 0. T by A6, RLVECT_1:10 ; :: thesis: verum

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

((||.h.|| ") (#) (R /* h)) . 0 = 0. T by A5;

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

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 A3, PARTFUN2:57;

A11: now :: thesis: for x being Point of S st x in Z /\ (dom f) holds

f /. x = r

A13:
the carrier of S --> (0. T) = L
by LOPBAN_1:31;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 A12, PARTFUN1:def 6

.= r by A10, A12 ;

:: thesis: verum

end;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 A12, PARTFUN1:def 6

.= r by A10, A12 ;

:: thesis: verum

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

f is_differentiable_in x0

hence A20:
f is_differentiable_on Z
by A1, A2, 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 A15: x0 in Z ; :: thesis: f is_differentiable_in x0

then consider N being Neighbourhood of x0 such that

A16: N c= Z by A1, Th2;

A17: N c= dom f by A2, A16;

A18: x0 in Z /\ (dom f) by A2, A15, XBOOLE_0:def 4;

for x being Point of S st x in N holds

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

end;assume A15: x0 in Z ; :: thesis: f is_differentiable_in x0

then consider N being Neighbourhood of x0 such that

A16: N c= Z by A1, Th2;

A17: N c= dom f by A2, A16;

A18: x0 in Z /\ (dom f) by A2, A15, XBOOLE_0:def 4;

for x being Point of S st x in N holds

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

proof

hence
f is_differentiable_in x0
by A17; :: thesis: verum
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 A4, PARTFUN1:def 6

.= 0. T ;

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

then x in Z /\ (dom f) by A16, A17, XBOOLE_0:def 4;

hence (f /. x) - (f /. x0) = r - (f /. x0) by A11

.= r - r by A11, A18

.= 0. T by RLVECT_1:15

.= (0. T) + (0. T) by RLVECT_1:4

.= (L . (x - x0)) + (R /. (x - x0)) by A13, A19 ;

:: thesis: verum

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

.= 0. T ;

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

then x in Z /\ (dom f) by A16, A17, XBOOLE_0:def 4;

hence (f /. x) - (f /. x0) = r - (f /. x0) by A11

.= r - r by A11, A18

.= 0. T by RLVECT_1:15

.= (0. T) + (0. T) by RLVECT_1:4

.= (L . (x - x0)) + (R /. (x - x0)) by A13, A19 ;

:: thesis: verum

(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))

let x0 be Point of S; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )

assume A21: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))

then consider N being Neighbourhood of x0 such that

A22: N c= Z by A1, Th2;

A23: N c= dom f by A2, A22;

A24: x0 in Z /\ (dom f) by A2, A21, XBOOLE_0:def 4;

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

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

proof

A27:
f is_differentiable_in x0
by A14, A21;
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 A4, PARTFUN1:def 6

.= 0. T ;

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

then x in Z /\ (dom f) by A22, A23, XBOOLE_0:def 4;

hence (f /. x) - (f /. x0) = r - (f /. x0) by A11

.= r - r by A11, A24

.= 0. T by RLVECT_1:15

.= (0. T) + (0. T) by RLVECT_1:4

.= (L . (x - x0)) + (R /. (x - x0)) by A13, A26 ;

:: thesis: verum

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

.= 0. T ;

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

then x in Z /\ (dom f) by A22, A23, XBOOLE_0:def 4;

hence (f /. x) - (f /. x0) = r - (f /. x0) by A11

.= r - r by A11, A24

.= 0. T by RLVECT_1:15

.= (0. T) + (0. T) by RLVECT_1:4

.= (L . (x - x0)) + (R /. (x - x0)) by A13, A26 ;

:: thesis: verum

thus (f `| Z) /. x0 = diff (f,x0) by A20, A21, Def9

.= 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) by A27, A23, A25, Def7 ; :: thesis: verum