theorem :: DIFF_2:4
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2))