let x0, x1 be Real; ( x0 in dom cosec & x1 in dom cosec implies [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) )
assume that
A1:
x0 in dom cosec
and
A2:
x1 in dom cosec
; [!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
A3: cosec . x1 =
(sin . x1) "
by A2, RFUNCT_1:def 2
.=
cosec x1
by XCMPLX_1:215
;
cosec . x0 =
(sin . x0) "
by A1, RFUNCT_1:def 2
.=
cosec x0
by XCMPLX_1:215
;
then [!cosec,x0,x1!] =
(((1 * (sin x1)) / ((sin x0) * (sin x1))) - (1 / (sin x1))) / (x0 - x1)
by A2, A3, RFUNCT_1:3, XCMPLX_1:91
.=
(((1 * (sin x1)) / ((sin x0) * (sin x1))) - ((1 * (sin x0)) / ((sin x1) * (sin x0)))) / (x0 - x1)
by A1, RFUNCT_1:3, XCMPLX_1:91
.=
(((sin x1) - (sin x0)) / ((sin x1) * (sin x0))) / (x0 - x1)
by XCMPLX_1:120
.=
((sin x1) - (sin x0)) / (((sin x1) * (sin x0)) * (x0 - x1))
by XCMPLX_1:78
.=
(2 * ((cos ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((sin x1) * (sin x0)) * (x0 - x1))
by SIN_COS4:16
;
hence
[!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
; verum