let m be non zero Element of NAT ; 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 ; 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); 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; ( 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 )
; 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
let I be non
empty FinSequence of
NAT ;
( 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 )
;
(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;
verum
end;
hence
f + g is_continuously_differentiable_up_to_order k,X
by A2, A1, PDIFF_9:85, XBOOLE_1:19; verum