theorem
Th5
:
:: INTEGR14:5
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
cosec
)
holds
(

(
ln
*
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(

(
ln
*
cosec
)
)
`
Z
)
.
x
=
cot
.
x
) )