let h, x be Real; for f being Function of REAL,REAL holds (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
let f be Function of REAL,REAL; (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
(fD (f,(h / 2))) . x = - ((bD (f,(- (h / 2)))) . x)
then (cD (f,h)) . x =
(- ((bD (f,(- (h / 2)))) . x)) - ((fD (f,(- (h / 2)))) . x)
by Th1
.=
(- ((bD (f,(- (h / 2)))) . x)) - (- ((bD (f,(h / 2))) . x))
by Th2
.=
((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
;
hence
(cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)
; verum