let h, x be Real; for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
let f be Function of REAL,REAL; ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
((fdif (f,h)) . 1) . x =
(fD (f,h)) . x
by DIFF_3:7
.=
(f . (x + h)) - (f . x)
by DIFF_1:3
.=
(((fdif (f,h)) . 0) . (x + h)) - (f . x)
by DIFF_1:def 6
.=
(((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
by DIFF_1:def 6
;
hence
((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
; verum