theorem Th3: :: DIFF_1:3

for h, x being Real
for f being Function of REAL,REAL holds (fD (f,h)) . x = (f . (x + h)) - (f . x)