theorem Th10: :: CKSPACE1:10

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 st f is_continuously_differentiable_up_to_order i,Z & j <= i holds
f is_continuously_differentiable_up_to_order j,Z by PDIFF_9:84, XXREAL_0:2;