theorem Th84: :: PDIFF_9:84

for m being non zero Element of NAT
for Z being set
for i, j being Nat
for f being PartFunc of (REAL m),REAL st f is_partial_differentiable_up_to_order i,Z & j <= i holds
f is_partial_differentiable_up_to_order j,Z by XXREAL_0:2;