let h, x be Real; :: thesis: for f being Function of REAL ,REAL st h <> 0 holds
[!f,(x - h),x,(x + h)!] = (((cdif f,h) . 2) . x) / ((2 * h) * h)
let f be Function of REAL ,REAL ; :: thesis: ( h <> 0 implies [!f,(x - h),x,(x + h)!] = (((cdif f,h) . 2) . x) / ((2 * h) * h) )
assume h <> 0 ; :: thesis: [!f,(x - h),x,(x + h)!] = (((cdif f,h) . 2) . x) / ((2 * h) * h)
then ( x - h <> x & x - h <> x + h & x <> x + h ) ;
then A1: x - h,x,x + h are_mutually_different by ZFMISC_1:def 5;
A2: (cdif f,h) . 1 is Function of REAL ,REAL by DIFF_1:19;
[!f,(x - h),x,(x + h)!] = [!f,(x + h),x,(x - h)!] by A1, DIFF_1:34
.= ([!f,x,(x + h)!] - [!f,x,(x - h)!]) / ((x + h) - (x - h)) by DIFF_1:29
.= ([!f,((x + (h / 2)) - (h / 2)),((x + (h / 2)) + (h / 2))!] - [!f,((x - (h / 2)) - (h / 2)),((x - (h / 2)) + (h / 2))!]) / ((x + h) - (x - h)) by DIFF_1:29
.= (((((cdif f,h) . 1) . (x + (h / 2))) / h) - [!f,((x - (h / 2)) - (h / 2)),((x - (h / 2)) + (h / 2))!]) / ((x + h) - (x - h)) by Th30
.= (((((cdif f,h) . 1) . (x + (h / 2))) / h) - ((((cdif f,h) . 1) . (x - (h / 2))) / h)) / ((x + h) - (x - h)) by Th30
.= (((((cdif f,h) . 1) . (x + (h / 2))) - (((cdif f,h) . 1) . (x - (h / 2)))) / h) / ((x + h) - (x - h))
.= (((cD ((cdif f,h) . 1),h) . x) / h) / (2 * h) by A2, DIFF_1:5
.= ((((cdif f,h) . (1 + 1)) . x) / h) / (2 * h) by DIFF_1:def 8
.= (((cdif f,h) . 2) . x) / ((2 * h) * h) by XCMPLX_1:79 ;
hence [!f,(x - h),x,(x + h)!] = (((cdif f,h) . 2) . x) / ((2 * h) * h) ; :: thesis: verum