theorem :: DIFF_3:7

for h being Real
for f being Function of REAL,REAL holds (fdif (f,h)) . 1 = fD (f,h)