theorem :: DIFF_1:18

for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (f . x) - ((Shift (f,(- h))) . x)