let m be non zero 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 A1: ( 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 11 :: 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 A2: ( 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 A1;
hence f + g is_partial_differentiable_on Z,I by A1, A2, Th75; :: thesis: verum
end;
let I be non empty FinSequence of NAT ; :: according to PDIFF_9:def 11 :: thesis: ( len I <= i & rng I c= Seg m implies f - g is_partial_differentiable_on Z,I )
assume A3: ( 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 A1;
hence f - g is_partial_differentiable_on Z,I by A1, A3, Th77; :: thesis: verum