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