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