let x, h be Real; :: thesis: for f being Function of REAL ,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & cos x <> 0 & cos (x + h) <> 0 holds
(fD f,h) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h))
let f be Function of REAL ,REAL ; :: thesis: ( ( for x being Real holds f . x = 1 / (cos x) ) & cos x <> 0 & cos (x + h) <> 0 implies (fD f,h) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h)) )
assume that
A1: for x being Real holds f . x = 1 / (cos x) and
A2: ( cos x <> 0 & cos (x + h) <> 0 ) ; :: thesis: (fD f,h) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h))
A3: f . (x + h) = 1 / (cos (x + h)) by A1;
(fD f,h) . x = (1 / (cos (x + h))) - (f . x) by A3, DIFF_1:3
.= (1 / (cos (x + h))) - (1 / (cos x)) by A1
.= ((1 * (cos x)) - (1 * (cos (x + h)))) / ((cos (x + h)) * (cos x)) by A2, XCMPLX_1:131
.= ((cos x) - (cos (x + h))) / ((1 / 2) * ((cos ((x + h) + x)) + (cos ((x + h) - x)))) by SIN_COS4:36
.= (((cos x) - (cos (x + h))) / (1 / 2)) / ((cos ((2 * x) + h)) + (cos h)) by XCMPLX_1:79
.= 2 * (((cos x) - (cos (x + h))) / ((cos ((2 * x) + h)) + (cos h))) ;
hence (fD f,h) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h)) ; :: thesis: verum