theorem
:: INTEGR15:14
for
n
being
Element
of
NAT
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
for
g
being
Function
of
A
,
(
REAL
n
)
st
f

A
=
g
holds
integral
(
f
,
A
)
=
integral
g