let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
let f be Function of REAL,REAL; :: thesis: (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
(bD ((bD (f,h)),h)) . x = ((bD (f,h)) . x) - ((bD (f,h)) . (x - h)) by DIFF_1:4
.= ((f . x) - (f . (x - h))) - ((bD (f,h)) . (x - h)) by DIFF_1:4
.= ((f . x) - (f . (x - h))) - ((f . (x - h)) - (f . ((x - h) - h))) by DIFF_1:4
.= (2 * ((f . x) - (f . (x - h)))) - ((f . x) - (f . (x - (2 * h))))
.= (2 * ((bD (f,h)) . x)) - ((f . x) - (f . (x - (2 * h)))) by DIFF_1:4
.= (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) by DIFF_1:4 ;
hence (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x) ; :: thesis: verum