let h, x be Real; for f being PartFunc of REAL,REAL st x + (h / 2) in dom f & x - (h / 2) in dom f holds
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
let f be PartFunc of REAL,REAL; ( x + (h / 2) in dom f & x - (h / 2) in dom f implies (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) )
assume A1:
( x + (h / 2) in dom f & x - (h / 2) in dom f )
; (cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
A2:
dom (Shift (f,(- (h / 2)))) = (- (- (h / 2))) ++ (dom f)
by Def1;
A3:
dom (Shift (f,(h / 2))) = (- (h / 2)) ++ (dom f)
by Def1;
A4:
(- (h / 2)) + (x + (h / 2)) in (- (h / 2)) ++ (dom f)
by A1, MEASURE6:46;
then A5:
(Shift (f,(h / 2))) . x = f . (x + (h / 2))
by Def1;
A6:
(h / 2) + (x - (h / 2)) in (- (- (h / 2))) ++ (dom f)
by A1, MEASURE6:46;
then A7:
(Shift (f,(- (h / 2)))) . x = f . (x + (- (h / 2)))
by Def1;
x in (dom (Shift (f,(h / 2)))) /\ (dom (Shift (f,(- (h / 2)))))
by A4, A6, A3, A2, XBOOLE_0:def 4;
then
x in dom (cD (f,h))
by VALUED_1:12;
hence
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))
by A7, A5, VALUED_1:13; verum