theorem Th50: :: NDIFF13:49

for i being Nat
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 i,Z & (diff (L1,i,Z)) `| Z is_continuous_on Z )