theorem Th4: :: NDIFF13:3

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S st f is_differentiable_on Z holds
(f | Z) `| Z = f `| Z