let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x)
let f be Function of REAL,REAL; :: thesis: (cD (f,h)) . x = ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x)
(cD (f,h)) . x = (((f . (x + (h / 2))) - (f . x)) + (f . x)) - (f . (x - (h / 2))) by DIFF_1:5
.= ((f . (x + (h / 2))) - (f . x)) - ((f . (x - (h / 2))) - (f . x))
.= ((fD (f,(h / 2))) . x) - ((f . (x - (h / 2))) - (f . x)) by DIFF_1:3
.= ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x) by DIFF_1:3 ;
hence (cD (f,h)) . x = ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x) ; :: thesis: verum