:: deftheorem defines bounded INTEGR19:def 1 :
for R being RealNormSpace
for X being non empty set
for g being PartFunc of X,R holds
( g is bounded iff ex r being Real st
for y being set st y in dom g holds
||.(g /. y).|| < r );