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
for I being non empty FinSequence of NAT st f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
let i, j be Element of NAT ; :: thesis: for Z being set
for f being PartFunc of (REAL m),REAL
for I being non empty FinSequence of NAT st f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
let Z be set ; :: thesis: for f being PartFunc of (REAL m),REAL
for I being non empty FinSequence of NAT st f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
let f be PartFunc of (REAL m),REAL; :: thesis: for I being non empty FinSequence of NAT st f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
let I be non empty FinSequence of NAT ; :: thesis: ( f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j implies f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z )
assume AS: ( f is_partial_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j ) ; :: thesis: f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z
let J be non empty FinSequence of NAT ; :: according to PDIFF_9:def 10 :: thesis: ( len J <= i & rng J c= Seg m implies f `partial| (Z,I) is_partial_differentiable_on Z,J )
assume AS1: ( len J <= i & rng J c= Seg m ) ; :: thesis: f `partial| (Z,I) is_partial_differentiable_on Z,J
reconsider G = I ^ J as non empty FinSequence of NAT ;
P1: rng G = (rng I) \/ (rng J) by FINSEQ_1:31;
len G = (len I) + (len J) by FINSEQ_1:22;
then ( len G <= i + j & rng G c= Seg m ) by AS1, P1, AS, XBOOLE_1:8, XREAL_1:6;
then f is_partial_differentiable_on Z,G by AS, TDef9;
hence f `partial| (Z,I) is_partial_differentiable_on Z,J by XCW040; :: thesis: verum