theorem
Th6
:
:: INTEGR14:6
for
n
being
Nat
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
n
)
*
cosec
)
& 1
<=
n
holds
(

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

(
(
#Z
n
)
*
cosec
)
)
`
Z
)
.
x
=
(
n
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
#Z
(
n
+
1
)
)
) )