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 A1: ( x0 in dom cot & x1 in dom cot ) ; :: thesis: [!cot ,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))
then A2: ( sin x0 <> 0 & sin x1 <> 0 ) by FDIFF_8:2;
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 ;
cot . x1 = (cos . x1) * ((sin . x1) " ) by A1, RFUNCT_1:def 4
.= (cos . x1) * (1 / (sin . x1)) by XCMPLX_1:217
.= cot x1 by XCMPLX_1:100 ;
then [!cot ,x0,x1!] = (- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) / (x0 - x1) by A2, A3, 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