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)

reconsider xx = x as Element of REAL by XREAL_0:def 1;

dom ((Shift (f,h)) - f) = REAL by FUNCT_2:def 1;

hence (fD (f,h)) . x = ((Shift (f,h)) . xx) - (f . xx) by VALUED_1:13

.= (f . (x + h)) - (f . x) by Def2 ;

:: thesis: verum

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

reconsider xx = x as Element of REAL by XREAL_0:def 1;

dom ((Shift (f,h)) - f) = REAL by FUNCT_2:def 1;

hence (fD (f,h)) . x = ((Shift (f,h)) . xx) - (f . xx) by VALUED_1:13

.= (f . (x + h)) - (f . x) by Def2 ;

:: thesis: verum