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_distinct 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:120
.= (((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:78
.= (((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