theorem Th4: :: DIFF_1:4
for h, x being Real
for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - (f . (x - h))