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