let m be non zero Element of NAT ; :: thesis: for Z being set
for i, j being Nat
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 i, j being Nat
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 Nat; :: 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 A1: ( 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 11 :: thesis: ( len J <= i & rng J c= Seg m implies f `partial| (Z,I) is_partial_differentiable_on Z,J )
assume A2: ( 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 ;
A3: 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 A2, A3, A1, XBOOLE_1:8, XREAL_1:6;
then f is_partial_differentiable_on Z,G by A1;
hence f `partial| (Z,I) is_partial_differentiable_on Z,J by Th80; :: thesis: verum