let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (fD (f,(- (h / 2)))) . x = - ((bD (f,(h / 2))) . x)
let f be Function of REAL,REAL; :: thesis: (fD (f,(- (h / 2)))) . x = - ((bD (f,(h / 2))) . x)
(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