let h, x be Real; :: thesis: for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
let f be Function of REAL,REAL; :: thesis: [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
[!f,(x - h),x!] = [!f,x,(x - h)!] by DIFF_1:29
.= ((bD (f,h)) . x) / h by DIFF_1:4
.= ((bD (((bdif (f,h)) . 0),h)) . x) / h by DIFF_1:def 7
.= (((bdif (f,h)) . (0 + 1)) . x) / h by DIFF_1:def 7 ;
hence [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h ; :: thesis: verum