theorem :: NDIFF13:7

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for k being Nat st f is_differentiable_on k,Z & diff (f,k,Z) is_continuous_on Z holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) is_continuous_on Z ) by Th7;