let S, T be RealNormSpace; 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; 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; ( 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
; ( 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
; ( 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
;
then reconsider R = R as RestFunc of S,T by Def5;
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;
A13:
the carrier of S --> (0. T) = L
by LOPBAN_1:31;
hence A20:
f is_differentiable_on Z
by A1, A2, Th31; for x being Point of S st x in Z holds
(f `| Z) /. x = 0. (R_NormSpace_of_BoundedLinearOperators (S,T))
let x0 be Point of S; ( x0 in Z implies (f `| Z) /. x0 = 0. (R_NormSpace_of_BoundedLinearOperators (S,T)) )
assume A21:
x0 in Z
; (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))
A27:
f is_differentiable_in x0
by A14, A21;
thus (f `| Z) /. x0 =
diff (f,x0)
by A20, A21, Def9
.=
0. (R_NormSpace_of_BoundedLinearOperators (S,T))
by A27, A23, A25, Def7
; verum