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