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 :: thesis: for i being Nat st i <= n - 1 holds
(diff ((f1 + f2),Z)) . i is_differentiable_on Z

let i be 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: i in NAT by ORDINAL1:def 12;
A5: (diff (f2,Z)) . i is_differentiable_on Z by A2, A3;
then A6: Z c= dom ((diff (f2,Z)) . i) by FDIFF_1:def 6;
i <= n by A3, WSIERP_1:18;
then A7: (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) by A1, A2, Th17, A4;
A8: (diff (f1,Z)) . i is_differentiable_on Z by A1, A3;
then Z c= dom ((diff (f1,Z)) . i) by FDIFF_1:def 6;
then Z c= (dom ((diff (f1,Z)) . i)) /\ (dom ((diff (f2,Z)) . i)) by A6, 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 A8, A5, A7, FDIFF_1:18; :: thesis: verum

end;

hence f1 + f2 is_differentiable_on n,Z ; :: thesis: verum