let n, i 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 & i <= n holds
(diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i)
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 & i <= n holds
(diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i)
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n implies (diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i) )
assume A1: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z ) ; :: thesis: ( not i <= n or (diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i) )
assume i <= n ; :: thesis: (diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i)
then ( f1 is_differentiable_on i,Z & f2 is_differentiable_on i,Z ) by A1, TAYLOR_1:23;
hence (diff (f1 + f2),Z) . i = ((diff f1,Z) . i) + ((diff f2,Z) . i) by Th15; :: thesis: verum