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