theorem
:: INTEGR15:20
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
A
being non
empty
closed_interval
Subset
of
REAL
for
a
,
b
being
Real
st
A
=
[.
b
,
a
.]
holds

(
integral
(
f
,
A
)
)
=
integral
(
f
,
a
,
b
)