theorem :: DIFF_1:39

for h, x being Real
for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))