theorem :: DIFF_3:24
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - h),x,(x + h)!] = (((cdif (f,h)) . 2) . x) / ((2 * h) * h)