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

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

(
cosec
*
ln
)
)
`
Z
)
.
x
=
(
cos
.
(
ln
.
x
)
)
/
(
x
*
(
(
sin
.
(
ln
.
x
)
)
^2
)
)
) )