let h, x be Real; :: thesis: for f being Function of REAL,REAL holds [!f,x,(x + h)!] = ((fD (f,h)) . x) / h
let f be Function of REAL,REAL; :: thesis: [!f,x,(x + h)!] = ((fD (f,h)) . x) / h
[!f,x,(x + h)!] = (- ((f . (x + h)) - (f . x))) / (- h)
.= ((f . (x + h)) - (f . x)) / h by XCMPLX_1:191
.= ((fD (f,h)) . x) / h by DIFF_1:3 ;
hence [!f,x,(x + h)!] = ((fD (f,h)) . x) / h ; :: thesis: verum