theorem Th23: :: DIFF_3:23

for h, x being Real
for f being Function of REAL,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif (f,h)) . 1) . x) / h