::
deftheorem
defines
bounded
INTEGR15:def 12 :
for
n
being
Element
of
NAT
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
Function
of
A
,
(
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
);