let k, x, h 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:131
.= (((- 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