theorem :: DIFF_2:39
for h, k being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x & x <> 0 & x - h <> 0 ) ) holds
for x being Real holds (bD (f,h)) . x = (- (k * h)) / ((x - h) * x) ;