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