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