let h, x be Real; :: thesis: 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; :: thesis: (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) ; :: thesis: verum