let m be non empty Element of NAT ; :: thesis: for i, j being Element of NAT
for Z being set
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
let i, j be Element of NAT ; :: thesis: for Z being set
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
let Z be set ; :: thesis: 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
let f be PartFunc of (REAL m),REAL; :: thesis: ( f is_partial_differentiable_up_to_order i,Z & j <= i implies f is_partial_differentiable_up_to_order j,Z )
assume AS: ( f is_partial_differentiable_up_to_order i,Z & j <= i ) ; :: thesis: f is_partial_differentiable_up_to_order j,Z
let I be non empty FinSequence of NAT ; :: according to PDIFF_9:def 10 :: thesis: ( len I <= j & rng I c= Seg m implies f is_partial_differentiable_on Z,I )
assume AS1: ( len I <= j & rng I c= Seg m ) ; :: thesis: f is_partial_differentiable_on Z,I
then len I <= i by AS, XXREAL_0:2;
hence f is_partial_differentiable_on Z,I by AS, AS1, TDef9; :: thesis: verum