let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h))

let f be Function of REAL,REAL; :: thesis: (bD (f,h)) . x = (f . x) - (f . (x - h))

thus (bD (f,h)) . x = (- (fD (f,(- h)))) . x by RFUNCT_1:19

.= - ((fD (f,(- h))) . x) by VALUED_1:8

.= - ((f . (x + (- h))) - (f . x)) by Th3

.= (f . x) - (f . (x - h)) ; :: thesis: verum

let f be Function of REAL,REAL; :: thesis: (bD (f,h)) . x = (f . x) - (f . (x - h))

thus (bD (f,h)) . x = (- (fD (f,(- h)))) . x by RFUNCT_1:19

.= - ((fD (f,(- h))) . x) by VALUED_1:8

.= - ((f . (x + (- h))) - (f . x)) by Th3

.= (f . x) - (f . (x - h)) ; :: thesis: verum