let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
let f be Function of REAL,REAL; :: thesis: (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
(fD (f,(h / 2))) . x = - ((bD (f,(- (h / 2)))) . x)

proof

(fD (f,(h / 2))) . x = (f . (x + (h / 2))) - (f . x) by DIFF_1:3
.= - ((f . x) - (f . (x - (- (h / 2)))))
.= - ((bD (f,(- (h / 2)))) . x) by DIFF_1:4 ;
hence (fD (f,(h / 2))) . x = - ((bD (f,(- (h / 2)))) . x) ; :: thesis: verum

end;

then (cD (f,h)) . x = (- ((bD (f,(- (h / 2)))) . x)) - ((fD (f,(- (h / 2)))) . x) by Th1
.= (- ((bD (f,(- (h / 2)))) . x)) - (- ((bD (f,(h / 2))) . x)) by Th2
.= ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x) ;
hence (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x) ; :: thesis: verum