let m be non zero Element of NAT ; :: thesis: for Z being non empty Subset of (REAL m)
for f being PartFunc of (REAL m),REAL
for i, j being Nat
for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z
let Z be non empty Subset of (REAL m); :: thesis: for f being PartFunc of (REAL m),REAL
for i, j being Nat
for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z
let f be PartFunc of (REAL m),REAL; :: thesis: for i, j being Nat
for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z
let i, j be Nat; :: thesis: for I being non empty FinSequence of NAT st f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j holds
f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z
let I be non empty FinSequence of NAT ; :: thesis: ( f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j implies f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z )
assume A1: ( f is_continuously_differentiable_up_to_order i + j,Z & rng I c= Seg m & len I = j ) ; :: thesis: f `partial| (Z,I) is_continuously_differentiable_up_to_order i,Z
then A2: ( Z c= dom f & f is_partial_differentiable_up_to_order i + j,Z & ( for I being non empty FinSequence of NAT st len I <= i + j & rng I c= Seg m holds
f `partial| (Z,I) is_continuous_on Z ) ) ;
A3: f is_partial_differentiable_on Z,I by A2, A1, NAT_1:11;
f is_partial_differentiable_on Z,I by A2, A1, NAT_1:11;
hence Z c= dom (f `partial| (Z,I)) by Th1; :: according to CKSPACE1:def 1 :: thesis: ( f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z & ( for I being non empty FinSequence of NAT st len I <= i & rng I c= Seg m holds
(f `partial| (Z,I)) `partial| (Z,I) is_continuous_on Z ) )
thus f `partial| (Z,I) is_partial_differentiable_up_to_order i,Z by PDIFF_9:83, A1; :: thesis: for I being non empty FinSequence of NAT st len I <= i & rng I c= Seg m holds
(f `partial| (Z,I)) `partial| (Z,I) is_continuous_on Z
let J be non empty FinSequence of NAT ; :: thesis: ( len J <= i & rng J c= Seg m implies (f `partial| (Z,I)) `partial| (Z,J) is_continuous_on Z )
assume A4: ( len J <= i & rng J c= Seg m ) ; :: thesis: (f `partial| (Z,I)) `partial| (Z,J) is_continuous_on Z
reconsider G = I ^ J as non empty FinSequence of NAT ;
A5: 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 A4, A5, A1, XBOOLE_1:8, XREAL_1:6;
then f `partial| (Z,G) is_continuous_on Z by A1;
hence (f `partial| (Z,I)) `partial| (Z,J) is_continuous_on Z by A3, Th7; :: thesis: verum