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 )) )
assume h <> 0 ; :: thesis: [!f,x,(x + h),(x + (2 * h))!] = (((fdif f,h) . 2) . x) / (2 * (h ^2 ))
then ( x <> x + h & x <> x + (2 * h) & x + h <> x + (2 * h) ) ;
then A1: x,x + h,x + (2 * h) are_mutually_different by ZFMISC_1:def 5;
A2: (fdif f,h) . 1 is Function of REAL ,REAL by DIFF_1:2;
[!f,x,(x + h),(x + (2 * h))!] = [!f,(x + (2 * h)),(x + h),x!] by A1, 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:121
.= (((fD ((fdif f,h) . 1),h) . x) / h) / (2 * h) by A2, 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:79
.= (((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