theorem :: NDIFF_1:33

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st Z is open & Z c= dom f & ex r being Point of T st rng f = {r} 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)) ) )