let h, x be Real; :: thesis: for f being Function of REAL,REAL holds (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

let f be Function of REAL,REAL; :: thesis: (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

reconsider xx = x as Element of REAL by XREAL_0:def 1;

dom ((Shift (f,(h / 2))) - (Shift (f,(- (h / 2))))) = REAL by FUNCT_2:def 1;

hence (cD (f,h)) . x = ((Shift (f,(h / 2))) . xx) - ((Shift (f,(- (h / 2)))) . xx) by VALUED_1:13

.= (f . (x + (h / 2))) - ((Shift (f,(- (h / 2)))) . x) by Def2

.= (f . (x + (h / 2))) - (f . (x + (- (h / 2)))) by Def2

.= (f . (x + (h / 2))) - (f . (x - (h / 2))) ;

:: thesis: verum

let f be Function of REAL,REAL; :: thesis: (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

reconsider xx = x as Element of REAL by XREAL_0:def 1;

dom ((Shift (f,(h / 2))) - (Shift (f,(- (h / 2))))) = REAL by FUNCT_2:def 1;

hence (cD (f,h)) . x = ((Shift (f,(h / 2))) . xx) - ((Shift (f,(- (h / 2)))) . xx) by VALUED_1:13

.= (f . (x + (h / 2))) - ((Shift (f,(- (h / 2)))) . x) by Def2

.= (f . (x + (h / 2))) - (f . (x + (- (h / 2)))) by Def2

.= (f . (x + (h / 2))) - (f . (x - (h / 2))) ;

:: thesis: verum