let h, x be Real; for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
let f be Function of REAL,REAL; (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
(bD (f,h)) . x =
((bdif (f,h)) . 1) . x
by DIFF_3:11
.=
(f . x) - ((Shift (f,(- h))) . x)
by DIFF_1:18
;
hence
(bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
; verum