let h, x be Real; for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
let f be Function of REAL,REAL; [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
[!f,x,(x + h)!] =
[!f,(x + h),x!]
by DIFF_1:29
.=
((fD (f,h)) . x) / h
by DIFF_1:3
.=
((fD (((fdif (f,h)) . 0),h)) . x) / h
by DIFF_1:def 6
.=
(((fdif (f,h)) . (0 + 1)) . x) / h
by DIFF_1:def 6
;
hence
[!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
; verum