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
(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:130
.= (((- 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