theorem
:: INTEGR14:23
for
A
being non
empty
closed_interval
Subset
of
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
sec
)
&
Z
=
dom
tan
&
tan

A
is
continuous
holds
integral
(
tan
,
A
)
=
(
(
ln
*
sec
)
.
(
upper_bound
A
)
)

(
(
ln
*
sec
)
.
(
lower_bound
A
)
)