theorem :: DIFF_1:26

for n being Nat
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . n) . x = ((bdif (f,h)) . n) . (x + (n * h))