let h, x be Real; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum

(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2)))

let f be PartFunc of REAL,REAL; :: thesis: ( 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 ) ; :: thesis: (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; :: thesis: verum