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