theorem
:: INTEGR15:23
for
n
being
Nat
for
Z
,
x
being
set
for
f
being
PartFunc
of
Z
,
(
REAL
n
)
for
r
being
Real
st
x
in
dom
(
r
(#)
f
)
holds
(
r
(#)
f
)
/.
x
=
r
*
(
f
/.
x
)