let x0, x1 be Real; ( x0 in dom cot & x1 in dom cot implies [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1))) )
assume A1:
( x0 in dom cot & x1 in dom cot )
; [!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
A2:
( sin x0 <> 0 & sin x1 <> 0 )
by A1, FDIFF_8:2;
[!(cot (#) cot),x0,x1!] =
(((cot . x0) * (cot . x0)) - ((cot (#) cot) . x1)) / (x0 - x1)
by VALUED_1:5
.=
(((cot . x0) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1)
by VALUED_1:5
.=
((((cos . x0) * ((sin . x0) ")) * (cot . x0)) - ((cot . x1) * (cot . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - ((cot . x1) * (cot . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
((((cos . x0) * ((sin . x0) ")) * ((cos . x0) * ((sin . x0) "))) - (((cos . x1) * ((sin . x1) ")) * (cot . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((cot x0) ^2) - ((cot x1) ^2)) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((cot x0) - (cot x1)) * ((cot x0) + (cot x1))) / (x0 - x1)
.=
((- ((sin (x0 - x1)) / ((sin x0) * (sin x1)))) * ((cot x0) + (cot x1))) / (x0 - x1)
by A2, SIN_COS4:24
.=
(- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((cot x0) + (cot x1)))) / (x0 - x1)
.=
(- (((sin (x0 - x1)) / ((sin x0) * (sin x1))) * ((sin (x0 + x1)) / ((sin x0) * (sin x1))))) / (x0 - x1)
by A2, SIN_COS4:23
.=
(- (((sin (x0 + x1)) * (sin (x0 - x1))) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1)
by XCMPLX_1:76
.=
(- ((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2))) / (x0 - x1)
by SIN_COS4:38
.=
- (((((cos x1) ^2) - ((cos x0) ^2)) / (((sin x0) * (sin x1)) ^2)) / (x0 - x1))
.=
- ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
by XCMPLX_1:78
;
hence
[!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
; verum