theorem Th17: :: NDIFF_6:17

for S, T being RealNormSpace
for f being PartFunc of S,T
for Z being Subset of S
for n being Nat st f is_differentiable_on n,Z holds
for m being Nat st m <= n holds
f is_differentiable_on m,Z