:: deftheorem defines BoundedFunctions C0SP1:def 13 :
for X being non empty set holds BoundedFunctions X = { f where f is Function of X,REAL : f | X is bounded } ;