theorem :: DIFF_1:36

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