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 1
.= (cos . x0) * (1 / (sin . x0)) by XCMPLX_1:215
.= cot x0 by XCMPLX_1:99 ;
A4: cot . x1 = (cos . x1) * ((sin . x1) ") by A2, RFUNCT_1:def 1
.= (cos . x1) * (1 / (sin . x1)) by XCMPLX_1:215
.= cot x1 by XCMPLX_1:99 ;
( 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:24
.= - (((sin (x0 - x1)) / ((sin x0) * (sin x1))) / (x0 - x1)) by XCMPLX_1:187 ;
hence [!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1))) by XCMPLX_1:78; :: thesis: verum