let h, x be Real; :: thesis: for f being Function of REAL ,REAL st h <> 0 holds
[!f,(x - (2 * h)),(x - h),x!] = (((bdif f,h) . 2) . x) / (2 * (h ^2 ))
let f be Function of REAL ,REAL ; :: thesis: ( h <> 0 implies [!f,(x - (2 * h)),(x - h),x!] = (((bdif f,h) . 2) . x) / (2 * (h ^2 )) )
set y = x - h;
A1: (bdif f,h) . 1 is Function of REAL ,REAL by DIFF_1:12;
assume A2: h <> 0 ; :: thesis: [!f,(x - (2 * h)),(x - h),x!] = (((bdif 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_different by A3, ZFMISC_1:def 5;
then [!f,(x - (2 * h)),(x - h),x!] = [!f,x,(x - h),(x - (2 * h))!] by DIFF_1:34
.= ([!f,(x - h),x!] - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by DIFF_1:29
.= (((((bdif f,h) . 1) . x) / h) - [!f,(x - h),(x - (2 * h))!]) / (x - (x - (2 * h))) by Th3
.= (((((bdif f,h) . 1) . x) / h) - [!f,((x - h) - h),(x - h)!]) / (x - (x - (2 * h))) by DIFF_1:29
.= (((((bdif f,h) . 1) . x) / h) - ((((bdif f,h) . 1) . (x - h)) / h)) / (x - (x - (2 * h))) by Th3
.= (((((bdif f,h) . 1) . x) - (((bdif f,h) . 1) . (x - h))) / h) / (x - (x - (2 * h))) by XCMPLX_1:121
.= (((bD ((bdif f,h) . 1),h) . x) / h) / (2 * h) by A1, DIFF_1:4
.= ((((bdif f,h) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def 7
.= (((bdif f,h) . 2) . x) / (h * (2 * h)) by XCMPLX_1:79
.= (((bdif f,h) . 2) . x) / (2 * (h ^2 )) ;
hence [!f,(x - (2 * h)),(x - h),x!] = (((bdif f,h) . 2) . x) / (2 * (h ^2 )) ; :: thesis: verum