theorem :: DIFF_3:40
for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x > 0 & x - h > 0 holds
(bD (f,h)) . x = (sqrt x) - (sqrt (x - h))