let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds (fD f,h) . x = (f . (x + h)) - (f . x)
let f be Function of REAL ,REAL ; :: thesis: (fD f,h) . x = (f . (x + h)) - (f . x)
dom ((Shift f,h) - f) = REAL by FUNCT_2:def 1;
hence (fD f,h) . x = ((Shift f,h) . x) - (f . x) by VALUED_1:13
.= (f . (x + h)) - (f . x) by Def2 ;
:: thesis: verum