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