theorem Th8: :: DIFF_1:8

for n being Nat
for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + f2),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (((fdif (f2,h)) . (n + 1)) . x)