let n be Element of NAT ; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
f1 + f2 is_differentiable_on n,Z
let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds
f1 + f2 is_differentiable_on n,Z
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1 + f2 is_differentiable_on n,Z )
assume that
A1: f1 is_differentiable_on n,Z and
A2: f2 is_differentiable_on n,Z ; :: thesis: f1 + f2 is_differentiable_on n,Z

now

let i be Element of NAT ; :: thesis: ( i <= n - 1 implies (diff (f1 + f2),Z) . i is_differentiable_on Z )
assume A3: i <= n - 1 ; :: thesis: (diff (f1 + f2),Z) . i is_differentiable_on Z
A4: (diff f2,Z) . i is_differentiable_on Z by A2, A3, TAYLOR_1:def 6;
then A5: Z c= dom ((diff f2,Z) . i) by FDIFF_1:def 7;
i <= n by A3, WSIERP_1:23;
then A6: (diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i) by A1, A2, Th17;
A7: (diff f1,Z) . i is_differentiable_on Z by A1, A3, TAYLOR_1:def 6;
then Z c= dom ((diff f1,Z) . i) by FDIFF_1:def 7;
then Z c= (dom ((diff f1,Z) . i)) /\ (dom ((diff f2,Z) . i)) by A5, XBOOLE_1:19;
then Z c= dom (((diff f1,Z) . i) + ((diff f2,Z) . i)) by VALUED_1:def 1;
hence (diff (f1 + f2),Z) . i is_differentiable_on Z by A7, A4, A6, FDIFF_1:26; :: thesis: verum

end;

hence f1 + f2 is_differentiable_on n,Z by TAYLOR_1:def 6; :: thesis: verum