theorem Th9: :: CKSPACE1:9

for m being non zero Element of NAT
for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i, j being Nat
for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z