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