theorem
:: INTEGR15:19
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
=
[.
a
,
b
.]
holds
integral
(
f
,
A
)
=
integral
(
f
,
a
,
b
)