let h, x be Real; for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos x <> 0 & cos (x + h) <> 0 holds
(fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)
let f be Function of REAL,REAL; ( ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos x <> 0 & cos (x + h) <> 0 implies (fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2) )
assume that
A1:
for x being Real holds f . x = 1 / ((cos x) ^2)
and
A2:
( cos x <> 0 & cos (x + h) <> 0 )
; (fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)
(fD (f,h)) . x =
(f . (x + h)) - (f . x)
by DIFF_1:3
.=
(1 / ((cos (x + h)) ^2)) - (f . x)
by A1
.=
(1 / ((cos (x + h)) ^2)) - (1 / ((cos x) ^2))
by A1
.=
((1 * ((cos x) ^2)) - (1 * ((cos (x + h)) ^2))) / (((cos (x + h)) ^2) * ((cos x) ^2))
by A2, XCMPLX_1:130
.=
(((cos x) ^2) - ((cos (x + h)) ^2)) / (((cos (x + h)) * (cos x)) ^2)
.=
(((cos x) ^2) - ((cos (x + h)) ^2)) / (((1 / 2) * ((cos ((x + h) + x)) + (cos ((x + h) - x)))) ^2)
by SIN_COS4:32
.=
(((cos x) ^2) - ((cos (x + h)) ^2)) / ((1 / 4) * (((cos ((2 * x) + h)) + (cos h)) ^2))
.=
((((cos x) ^2) - ((cos (x + h)) ^2)) / (1 / 4)) / (((cos ((2 * x) + h)) + (cos h)) ^2)
by XCMPLX_1:78
.=
4 * ((((cos x) - (cos (x + h))) * ((cos x) + (cos (x + h)))) / (((cos ((2 * x) + h)) + (cos h)) ^2))
.=
4 * (((- (2 * ((sin ((x + (x + h)) / 2)) * (sin ((x - (x + h)) / 2))))) * ((cos x) + (cos (x + h)))) / (((cos ((2 * x) + h)) + (cos h)) ^2))
by SIN_COS4:18
.=
4 * (((- (2 * ((sin (((2 * x) + h) / 2)) * (sin ((- h) / 2))))) * (2 * ((cos (((2 * x) + h) / 2)) * (cos ((- h) / 2))))) / (((cos ((2 * x) + h)) + (cos h)) ^2))
by SIN_COS4:17
.=
(((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)
;
hence
(fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)
; verum