theorem Th1: :: DIFF_2:1

for h, x being Real
for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h