theorem Th51: :: NDIFF13:50

for n being Nat
for S being RealNormSpace
for Z being Subset of S
for f being PartFunc of S,S st Z is open & f = id ([#] S) holds
( f is_differentiable_on n,Z & diff (f,n,Z) is_continuous_on Z )