let h, x be Real; :: thesis: for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x + (h / 2) > 0 & x - (h / 2) > 0 holds
(cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2)))
let f be Function of REAL,REAL; :: thesis: ( ( for x being Real holds f . x = sqrt x ) & x + (h / 2) > 0 & x - (h / 2) > 0 implies (cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2))) )
assume A1: for x being Real holds f . x = sqrt x ; :: thesis: ( not x + (h / 2) > 0 or not x - (h / 2) > 0 or (cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2))) )
(cD (f,h)) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (sqrt (x + (h / 2))) - (f . (x - (h / 2))) by A1
.= (sqrt (x + (h / 2))) - (sqrt (x - (h / 2))) by A1 ;
hence ( not x + (h / 2) > 0 or not x - (h / 2) > 0 or (cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2))) ) ; :: thesis: verum