let h, x 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
(bD (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 (bD (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 )
; (bD (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)
(bD (f,h)) . x =
(f . x) - (f . (x - h))
by DIFF_1:4
.=
(1 / ((sin x) ^2)) - (f . (x - h))
by A1
.=
(1 / ((sin x) ^2)) - (1 / ((sin (x - h)) ^2))
by A1
.=
((1 * ((sin (x - h)) ^2)) - (1 * ((sin x) ^2))) / (((sin x) ^2) * ((sin (x - h)) ^2))
by A2, XCMPLX_1:130
.=
(((sin (x - h)) ^2) - ((sin x) ^2)) / (((sin x) * (sin (x - h))) ^2)
.=
(((sin (x - h)) ^2) - ((sin x) ^2)) / ((- ((1 / 2) * ((cos (x + (x - h))) - (cos (x - (x - h)))))) ^2)
by SIN_COS4:29
.=
(((sin (x - h)) ^2) - ((sin x) ^2)) / ((1 / 4) * (((cos ((2 * x) - h)) - (cos h)) ^2))
.=
((((sin (x - h)) ^2) - ((sin x) ^2)) / (1 / 4)) / (((cos ((2 * x) - h)) - (cos h)) ^2)
by XCMPLX_1:78
.=
4 * ((((sin (x - h)) - (sin x)) * ((sin (x - h)) + (sin x))) / (((cos ((2 * x) - h)) - (cos h)) ^2))
.=
4 * (((2 * ((cos (((x - h) + x) / 2)) * (sin (((x - h) - x) / 2)))) * ((sin (x - h)) + (sin x))) / (((cos ((2 * x) - h)) - (cos h)) ^2))
by SIN_COS4:16
.=
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:15
.=
((((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
(bD (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