let S, T be RealNormSpace; :: thesis: for Z being Subset of S
for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
f + g is_differentiable_on n,Z
let Z be Subset of S; :: thesis: for n being Nat
for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
f + g is_differentiable_on n,Z
let n be Nat; :: thesis: for f, g being PartFunc of S,T st 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z holds
f + g is_differentiable_on n,Z
let f, g be PartFunc of S,T; :: thesis: ( 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z implies f + g is_differentiable_on n,Z )
assume A1: ( 1 <= n & f is_differentiable_on n,Z & g is_differentiable_on n,Z ) ; :: thesis: f + g is_differentiable_on n,Z
then A2: Z is open by Th18;
Z /\ Z c= (dom f) /\ (dom g) by A1, XBOOLE_1:19;
then A3: Z c= dom (f + g) by VFUNCT_1:def 1;
for i being Nat st i <= n - 1 holds
diff ((f + g),i,Z) is_differentiable_on Z

proof

let i be Nat; :: thesis: ( i <= n - 1 implies diff ((f + g),i,Z) is_differentiable_on Z )
assume A4: i <= n - 1 ; :: thesis: diff ((f + g),i,Z) is_differentiable_on Z
then A5: ( diff (f,i,Z) is_differentiable_on Z & diff (g,i,Z) is_differentiable_on Z ) by Th14, A1;
n - 1 <= n by XREAL_1:43;
then A6: i <= n by A4, XXREAL_0:2;
then ( dom (diff (f,i,Z)) = Z & dom (diff (g,i,Z)) = Z ) by Th19, A1;
then Z /\ Z c= (dom (diff (f,i,Z))) /\ (dom (diff (g,i,Z))) ;
then Z c= dom ((diff (f,i,Z)) + (diff (g,i,Z))) by VFUNCT_1:def 1;
then (diff (f,i,Z)) + (diff (g,i,Z)) is_differentiable_on Z by A2, A5, NDIFF_1:39;
hence diff ((f + g),i,Z) is_differentiable_on Z by A1, A6, Th20; :: thesis: verum

end;

hence f + g is_differentiable_on n,Z by Th14, A3; :: thesis: verum