theorem Th3: :: DIFF_2:3

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