theorem
:: INTEGR14:21
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
exp_R
*
sec
)
(#)
(
sin
/
(
cos
^2
)
)
&
Z
=
dom
f
&
f

A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
exp_R
*
sec
)
.
(
upper_bound
A
)
)

(
(
exp_R
*
sec
)
.
(
lower_bound
A
)
)