theorem :: DIFF_1:10

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