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