::
deftheorem
defines
bounded
INTEGR15:def 15 :
for
n
being
Element
of
NAT
for
f
being
PartFunc
of
REAL
,
(
REAL
n
)
holds
(
f
is
bounded
iff for
i
being
Element
of
NAT
st
i
in
Seg
n
holds
(
proj
(
i
,
n
)
)
*
f
is
bounded
);