let x, h be Real; 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; ( x in dom f & x + h in dom f implies (fD (f,h)) . x = (f . (x + h)) - (f . x) )
assume A0:
( x in dom f & x + h in dom f )
; (fD (f,h)) . x = (f . (x + h)) - (f . x)
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 (fD (f,h))
by VALUED_1:12;
hence
(fD (f,h)) . x = (f . (x + h)) - (f . x)
by A2, VALUED_1:13; verum