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
(bD f,h) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^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 (bD f,h) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 ) )
assume that
A1: for x being Real holds f . x = k / (x ^2 ) and
A2: ( x <> 0 & x - h <> 0 ) ; :: thesis: (bD f,h) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 )
A3: f . (x - h) = k / ((x - h) ^2 ) by A1;
(bD f,h) . x = (f . x) - (f . (x - h)) by DIFF_1:4
.= (k / (x ^2 )) - (k / ((x - h) ^2 )) by A1, A3
.= ((k * ((x - h) ^2 )) - (k * (x ^2 ))) / ((x ^2 ) * ((x - h) ^2 )) by A2, XCMPLX_1:131
.= (((- k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 ) ;
hence (bD f,h) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2 ) - (x * h)) ^2 ) ; :: thesis: verum