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