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