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

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