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