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