theorem Th9: :: NDIFF13:8

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 holds
for i being Nat st f is_differentiable_on i,X holds
( f is_differentiable_on i,Z & diff (f,i,Z) = (diff (f,i,X)) | Z )