let x0, x1 be Real; :: thesis: ( 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 A1: ( x0 in dom cosec & x1 in dom cosec ) ; :: thesis: [!cosec ,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
then A2: cosec . x0 = (sin . x0) " by RFUNCT_1:def 8
.= cosec x0 by XCMPLX_1:217 ;
cosec . x1 = (sin . x1) " by A1, RFUNCT_1:def 8
.= cosec x1 by XCMPLX_1:217 ;
then [!cosec ,x0,x1!] = (((1 * (sin x1)) / ((sin x0) * (sin x1))) - (1 / (sin x1))) / (x0 - x1) by A1, A2, RFUNCT_1:13, XCMPLX_1:92
.= (((1 * (sin x1)) / ((sin x0) * (sin x1))) - ((1 * (sin x0)) / ((sin x1) * (sin x0)))) / (x0 - x1) by A1, RFUNCT_1:13, XCMPLX_1:92
.= (((sin x1) - (sin x0)) / ((sin x1) * (sin x0))) / (x0 - x1) by XCMPLX_1:121
.= ((sin x1) - (sin x0)) / (((sin x1) * (sin x0)) * (x0 - x1)) by XCMPLX_1:79
.= (2 * ((cos ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((sin x1) * (sin x0)) * (x0 - x1)) by SIN_COS4:20 ;
hence [!cosec ,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1)) ; :: thesis: verum