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