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