:: 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 );