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