let n, i be Element of NAT ; 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; 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; ( 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 )
; ( not i <= n or (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) )
assume
i <= n
; (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; verum