let h, x be Real; :: thesis: for f being Function of REAL ,REAL holds ((cdif f,h) . 1) . x = ((Shift f,(h / 2)) . x) - ((Shift f,(- (h / 2))) . x)
let f be Function of REAL ,REAL ; :: thesis: ((cdif f,h) . 1) . x = ((Shift f,(h / 2)) . x) - ((Shift f,(- (h / 2))) . x)
set f2 = Shift f,(- (h / 2));
set f1 = Shift f,(h / 2);
((cdif f,h) . 1) . x = ((cdif f,h) . (0 + 1)) . x
.= (cD ((cdif f,h) . 0 ),h) . x by Def8
.= (cD f,h) . x by Def8
.= (f . (x + (h / 2))) - (f . (x - (h / 2))) by Th5
.= ((Shift f,(h / 2)) . x) - (f . (x + (- (h / 2)))) by Def2
.= ((Shift f,(h / 2)) . x) - ((Shift f,(- (h / 2))) . x) by Def2 ;
hence ((cdif f,h) . 1) . x = ((Shift f,(h / 2)) . x) - ((Shift f,(- (h / 2))) . x) ; :: thesis: verum