let h, x be Real; :: thesis: for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
let f be Function of REAL,REAL; :: thesis: ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
((cdif (f,h)) . 1) . x = (cD (f,h)) . x by DIFF_3:16
.= (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (((cdif (f,h)) . 0) . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:def 8
.= (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) by DIFF_1:def 8 ;
hence ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2))) ; :: thesis: verum