let h, x be Real; :: thesis: for f being PartFunc of REAL,REAL st x in dom f & x + h in dom f holds

(fD (f,h)) . x = (f . (x + h)) - (f . x)

let f be PartFunc of REAL,REAL; :: thesis: ( x in dom f & x + h in dom f implies (fD (f,h)) . x = (f . (x + h)) - (f . x) )

assume A1: ( x in dom f & x + h in dom f ) ; :: thesis: (fD (f,h)) . x = (f . (x + h)) - (f . x)

A2: dom (Shift (f,h)) = (- h) ++ (dom f) by Def1;

A3: (- h) + (x + h) in (- h) ++ (dom f) by A1, MEASURE6:46;

then A4: (Shift (f,h)) . x = f . (x + h) by Def1;

x in (dom (Shift (f,h))) /\ (dom f) by A3, A2, A1, XBOOLE_0:def 4;

then x in dom (fD (f,h)) by VALUED_1:12;

hence (fD (f,h)) . x = (f . (x + h)) - (f . x) by A4, VALUED_1:13; :: thesis: verum

(fD (f,h)) . x = (f . (x + h)) - (f . x)

let f be PartFunc of REAL,REAL; :: thesis: ( x in dom f & x + h in dom f implies (fD (f,h)) . x = (f . (x + h)) - (f . x) )

assume A1: ( x in dom f & x + h in dom f ) ; :: thesis: (fD (f,h)) . x = (f . (x + h)) - (f . x)

A2: dom (Shift (f,h)) = (- h) ++ (dom f) by Def1;

A3: (- h) + (x + h) in (- h) ++ (dom f) by A1, MEASURE6:46;

then A4: (Shift (f,h)) . x = f . (x + h) by Def1;

x in (dom (Shift (f,h))) /\ (dom f) by A3, A2, A1, XBOOLE_0:def 4;

then x in dom (fD (f,h)) by VALUED_1:12;

hence (fD (f,h)) . x = (f . (x + h)) - (f . x) by A4, VALUED_1:13; :: thesis: verum