let h, x be Real; :: thesis: 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))
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = sqrt x ) & x > 0 & x - h > 0 implies (bD (f,h)) . x = (sqrt x) - (sqrt (x - h)) )
assume A1: for x being Real holds f . x = sqrt x ; :: thesis: ( not x > 0 or not x - h > 0 or (bD (f,h)) . x = (sqrt x) - (sqrt (x - h)) )
(bD (f,h)) . x = (f . x) - (f . (x - h)) by DIFF_1:4
.= (sqrt x) - (f . (x - h)) by A1
.= (sqrt x) - (sqrt (x - h)) by A1 ;
hence ( not x > 0 or not x - h > 0 or (bD (f,h)) . x = (sqrt x) - (sqrt (x - h)) ) ; :: thesis: verum