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