theorem Th5: :: NDIFF13:4

for S, T being RealNormSpace
for f being PartFunc of S,T
for X, Z being Subset of S st Z is open & Z c= X & f is_differentiable_on X holds
f `| Z = (f `| X) | Z