let h, k 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:91

.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - ((k * (x + (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) by A2, XCMPLX_1:91

.= (((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2))) by XCMPLX_1:120 ;

hence (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ; :: thesis: verum

( 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:91

.= ((k * (x - (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) - ((k * (x + (h / 2))) / ((x - (h / 2)) * (x + (h / 2)))) by A2, XCMPLX_1:91

.= (((k * x) - (k * (h / 2))) - (k * (x + (h / 2)))) / ((x - (h / 2)) * (x + (h / 2))) by XCMPLX_1:120 ;

hence (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2))) ; :: thesis: verum