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