theorem Th3: :: NDIFF13:2

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