theorem Th48: :: NDIFF13:47

for E, F being RealNormSpace
for Z being non empty Subset of E
for L1 being PartFunc of E,F
for L0 being Point of F st Z is open & L1 = Z --> L0 holds
( L1 is_differentiable_on Z & L1 `| Z is_continuous_on Z & L1 `| Z = Z --> (0. (R_NormSpace_of_BoundedLinearOperators (E,F))) )