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