theorem
Th16
:
:: INTEGR15:16
for
Z
being
set
for
n
,
i
being
Element
of
NAT
for
r
being
Real
for
f
being
PartFunc
of
Z
,
(
REAL
n
)
holds
(
proj
(
i
,
n
)
)
*
(
r
(#)
f
)
=
r
(#)
(
(
proj
(
i
,
n
)
)
*
f
)