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