let h, x be Real; :: thesis: for f being Function of REAL,REAL st h <> 0 holds
[!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
let f be Function of REAL,REAL; :: thesis: ( h <> 0 implies [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) )
A1: (fdif (f,h)) . 1 is Function of REAL,REAL by DIFF_1:2;
assume A2: h <> 0 ; :: thesis: [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
then A3: x + h <> x + (2 * h) ;
( x <> x + h & x <> x + (2 * h) ) by A2;
then x,x + h,x + (2 * h) are_mutually_distinct by A3, ZFMISC_1:def 5;
then [!f,x,(x + h),(x + (2 * h))!] = [!f,(x + (2 * h)),(x + h),x!] by DIFF_1:34
.= ([!f,(x + h),(x + (2 * h))!] - [!f,(x + h),x!]) / ((x + (2 * h)) - x) by DIFF_1:29
.= ([!f,(x + h),((x + h) + h)!] - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by DIFF_1:29
.= (((((fdif (f,h)) . 1) . (x + h)) / h) - [!f,x,(x + h)!]) / ((x + (2 * h)) - x) by Th1
.= (((((fdif (f,h)) . 1) . (x + h)) / h) - ((((fdif (f,h)) . 1) . x) / h)) / ((x + (2 * h)) - x) by Th1
.= (((((fdif (f,h)) . 1) . (x + h)) - (((fdif (f,h)) . 1) . x)) / h) / ((x + (2 * h)) - x) by XCMPLX_1:120
.= (((fD (((fdif (f,h)) . 1),h)) . x) / h) / (2 * h) by A1, DIFF_1:3
.= ((((fdif (f,h)) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def 6
.= (((fdif (f,h)) . 2) . x) / (h * (2 * h)) by XCMPLX_1:78
.= (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ;
hence [!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2)) ; :: thesis: verum