theorem :: DIFF_1:11
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = ((Shift (f,h)) . x) - (f . x)