theorem :: DIFF_3:19

for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2))