let m be non zero Element of NAT ; :: thesis: for k being Element of NAT

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let k be Element of NAT ; :: thesis: for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let X be non empty Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open implies f + g is_continuously_differentiable_up_to_order k,X )

assume A1: ( f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open ) ; :: thesis: f + g is_continuously_differentiable_up_to_order k,X

A2: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

(f + g) `partial| (X,I) is_continuous_on X

for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let k be Element of NAT ; :: thesis: for X being non empty Subset of (REAL m)

for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let X be non empty Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),REAL st f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open holds

f + g is_continuously_differentiable_up_to_order k,X

let f, g be PartFunc of (REAL m),REAL; :: thesis: ( f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open implies f + g is_continuously_differentiable_up_to_order k,X )

assume A1: ( f is_continuously_differentiable_up_to_order k,X & g is_continuously_differentiable_up_to_order k,X & X is open ) ; :: thesis: f + g is_continuously_differentiable_up_to_order k,X

A2: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

for I being non empty FinSequence of NAT st len I <= k & rng I c= Seg m holds

(f + g) `partial| (X,I) is_continuous_on X

proof

hence
f + g is_continuously_differentiable_up_to_order k,X
by A2, A1, PDIFF_9:85, XBOOLE_1:19; :: thesis: verum
let I be non empty FinSequence of NAT ; :: thesis: ( len I <= k & rng I c= Seg m implies (f + g) `partial| (X,I) is_continuous_on X )

assume A3: ( len I <= k & rng I c= Seg m ) ; :: thesis: (f + g) `partial| (X,I) is_continuous_on X

A4: f is_partial_differentiable_on X,I by A3, PDIFF_9:def 11, A1;

A5: g is_partial_differentiable_on X,I by A3, A1, PDIFF_9:def 11;

reconsider f0 = f `partial| (X,I) as PartFunc of (REAL m),REAL ;

reconsider g0 = g `partial| (X,I) as PartFunc of (REAL m),REAL ;

A6: X = dom f0 by Th1, A3, PDIFF_9:def 11, A1;

A7: X = dom g0 by Th1, A3, A1, PDIFF_9:def 11;

A8: f0 is_continuous_on X by A3, A1;

A9: g0 is_continuous_on X by A3, A1;

f0 + g0 is_continuous_on X by A8, A9, A6, A7, PDIFF_9:46;

hence (f + g) `partial| (X,I) is_continuous_on X by A1, A3, A4, A5, PDIFF_9:75; :: thesis: verum

end;assume A3: ( len I <= k & rng I c= Seg m ) ; :: thesis: (f + g) `partial| (X,I) is_continuous_on X

A4: f is_partial_differentiable_on X,I by A3, PDIFF_9:def 11, A1;

A5: g is_partial_differentiable_on X,I by A3, A1, PDIFF_9:def 11;

reconsider f0 = f `partial| (X,I) as PartFunc of (REAL m),REAL ;

reconsider g0 = g `partial| (X,I) as PartFunc of (REAL m),REAL ;

A6: X = dom f0 by Th1, A3, PDIFF_9:def 11, A1;

A7: X = dom g0 by Th1, A3, A1, PDIFF_9:def 11;

A8: f0 is_continuous_on X by A3, A1;

A9: g0 is_continuous_on X by A3, A1;

f0 + g0 is_continuous_on X by A8, A9, A6, A7, PDIFF_9:46;

hence (f + g) `partial| (X,I) is_continuous_on X by A1, A3, A4, A5, PDIFF_9:75; :: thesis: verum