theorem :: DIFF_2:38
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 (fD (f,h)) . x = (- (k * h)) / ((x + h) * x) ;