let m be non empty Element of NAT ; :: thesis: for i being Element of NAT
for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open & f is_partial_differentiable_up_to_order i,X & g is_partial_differentiable_up_to_order i,X holds
( f + g is_partial_differentiable_up_to_order i,X & f - g is_partial_differentiable_up_to_order i,X )
let i be Element of NAT ; :: thesis: for X being Subset of (REAL m)
for f, g being PartFunc of (REAL m),REAL st X is open & f is_partial_differentiable_up_to_order i,X & g is_partial_differentiable_up_to_order i,X holds
( f + g is_partial_differentiable_up_to_order i,X & f - g is_partial_differentiable_up_to_order i,X )
let Z be Subset of (REAL m); :: thesis: for f, g being PartFunc of (REAL m),REAL st Z is open & f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z holds
( f + g is_partial_differentiable_up_to_order i,Z & f - g is_partial_differentiable_up_to_order i,Z )
let f, g be PartFunc of (REAL m),REAL; :: thesis: ( Z is open & f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z implies ( f + g is_partial_differentiable_up_to_order i,Z & f - g is_partial_differentiable_up_to_order i,Z ) )
assume AS: ( Z is open & f is_partial_differentiable_up_to_order i,Z & g is_partial_differentiable_up_to_order i,Z ) ; :: thesis: ( f + g is_partial_differentiable_up_to_order i,Z & f - g is_partial_differentiable_up_to_order i,Z )

hereby :: according to PDIFF_9:def 10 :: thesis: f - g is_partial_differentiable_up_to_order i,Z

let I be non empty FinSequence of NAT ; :: thesis: ( len I <= i & rng I c= Seg m implies f + g is_partial_differentiable_on Z,I )
assume P1: ( len I <= i & rng I c= Seg m ) ; :: thesis: f + g is_partial_differentiable_on Z,I
then ( f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) by AS, TDef9;
hence f + g is_partial_differentiable_on Z,I by AS, P1, XCW011; :: thesis: verum

end;

let I be non empty FinSequence of NAT ; :: according to PDIFF_9:def 10 :: thesis: ( len I <= i & rng I c= Seg m implies f - g is_partial_differentiable_on Z,I )
assume P1: ( len I <= i & rng I c= Seg m ) ; :: thesis: f - g is_partial_differentiable_on Z,I
then ( f is_partial_differentiable_on Z,I & g is_partial_differentiable_on Z,I ) by AS, TDef9;
hence f - g is_partial_differentiable_on Z,I by AS, P1, XCW021; :: thesis: verum