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