let h, k, x be Real; :: thesis: 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; :: thesis: ( ( 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 ) ; :: thesis: (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) ; :: thesis: verum