let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds (cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
let f be Function of REAL ,REAL ; :: thesis: (cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
dom ((Shift f,(h / 2)) - (Shift f,(- (h / 2)))) = REAL by FUNCT_2:def 1;
hence (cD f,h) . x = ((Shift f,(h / 2)) . x) - ((Shift f,(- (h / 2))) . x) by VALUED_1:13
.= (f . (x + (h / 2))) - ((Shift f,(- (h / 2))) . x) by Def2
.= (f . (x + (h / 2))) - (f . (x + (- (h / 2)))) by Def2
.= (f . (x + (h / 2))) - (f . (x - (h / 2))) ;
:: thesis: verum