theorem :: DIFF_4:39
for h, x being Real
for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)