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