theorem
:: INTEGR15:18
for
n
being
Element
of
NAT
for
r
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
st
A
c=
dom
f
&
f
is_integrable_on
A
&
f

A
is
bounded
holds
(
r
(#)
f
is_integrable_on
A
&
integral
(
(
r
(#)
f
)
,
A
)
=
r
*
(
integral
(
f
,
A
)
)
)