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