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