theorem Th17: :: HFDIFF_1:17

for n, i being 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)