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