let x0, x1 be Real; :: thesis: ( x0 in dom cot & x1 in dom cot implies [!cot ,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) )
assume that
A1: x0 in dom cot and
A2: x1 in dom cot ; :: thesis: [!cot ,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))
A3: cot . x0 = (cos . x0) * ((sin . x0) " ) by A1, RFUNCT_1:def 4
.= (cos . x0) * (1 / (sin . x0)) by XCMPLX_1:217
.= cot x0 by XCMPLX_1:100 ;
A4: cot . x1 = (cos . x1) * ((sin . x1) " ) by A2, RFUNCT_1:def 4
.= (cos . x1) * (1 / (sin . x1)) by XCMPLX_1:217
.= cot x1 by XCMPLX_1:100 ;
( sin x0 <> 0 & sin x1 <> 0 ) by A1, A2, FDIFF_8:2;
then [!cot ,x0,x1!] = (- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) / (x0 - x1) by A3, A4, SIN_COS4:28
.= - (((sin (x0 - x1)) / ((sin x0) * (sin x1))) / (x0 - x1)) by XCMPLX_1:188 ;
hence [!cot ,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) by XCMPLX_1:79; :: thesis: verum