let h, x 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 A1:
( x in dom f & x + h in dom f )
; (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; verum