let x, h 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:192
.= ((fD f,h) . x) / h by DIFF_1:3 ;
hence [!f,x,(x + h)!] = ((fD f,h) . x) / h ; :: thesis: verum