theorem Th7: :: NDIFF13:6

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 holds
( f | Z is_differentiable_on k,Z & diff ((f | Z),k,Z) = diff (f,k,Z) )