let x0, x1 be Real; ( x0 in dom cot & x1 in dom cot implies [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!] )
assume A1:
( x0 in dom cot & x1 in dom cot )
; [!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!]
[!((cot (#) cot) (#) sin),x0,x1!] =
((((cot (#) cot) . x0) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1)
by VALUED_1:5
.=
((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) (#) sin) . x1)) / (x0 - x1)
by VALUED_1:5
.=
((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot (#) cot) . x1) * (sin . x1))) / (x0 - x1)
by VALUED_1:5
.=
((((cot . x0) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1)
by VALUED_1:5
.=
(((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - (((cot . x1) * (cot . x1)) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((((cos . x0) * ((sin . x0) ")) * (cot . x0)) * (sin . x0)) - ((((cos . x1) * ((sin . x1) ")) * (cot . x1)) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
((((cot . x0) * (cos . x0)) * ((sin . x0) * (1 / (sin . x0)))) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1)
.=
((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * ((sin . x1) * (1 / (sin . x1))))) / (x0 - x1)
by A1, FDIFF_8:2, XCMPLX_1:106
.=
((((cot . x0) * (cos . x0)) * 1) - (((cot . x1) * (cos . x1)) * 1)) / (x0 - x1)
by A1, FDIFF_8:2, XCMPLX_1:106
.=
(((cot (#) cos) . x0) - ((cot . x1) * (cos . x1))) / (x0 - x1)
by VALUED_1:5
.=
[!(cot (#) cos),x0,x1!]
by VALUED_1:5
;
hence
[!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!]
; verum