let x, h be Real; :: thesis: 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 ; :: thesis: [!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 ; :: thesis: verum