let k, h be Real; :: thesis: for f being Function of REAL , REAL st ( for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) holds
for x being Real holds (cD f,h) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
let f be Function of REAL , REAL ; :: thesis: ( ( for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ) implies for x being Real holds (cD f,h) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) )
assume A1: for x being Real holds
( f . x = k / x & x + (h / 2) <> 0 & x - (h / 2) <> 0 ) ; :: thesis: for x being Real holds (cD f,h) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
let x be Real; :: thesis: (cD f,h) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
A2: x + (h / 2) <> 0 by A1;
A3: x - (h / 2) <> 0 by A1;
(cD f,h) . x = (f . (x + (h / 2))) - (f . (x - (h / 2))) by DIFF_1:5
.= (k / (x + (h / 2))) - (f . (x - (h / 2))) by A1
.= (k / (x + (h / 2))) - (k / (x - (h / 2))) by A1
.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - (k / (x - (h / 2))) by A3, XCMPLX_1:92
.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - ((k * (x + (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) by A2, XCMPLX_1:92
.= (((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2))) by XCMPLX_1:121 ;
hence (cD f,h) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ; :: thesis: verum