:: deftheorem defines is_bounded_on VFUNCT_1:def 6 :
for C being non empty set
for V being non empty NORMSTR
for f being PartFunc of C,V
for Y being set holds
( f is_bounded_on Y iff ex r being Real st
for c being Element of C st c in Y /\ (dom f) holds
||.(f /. c).|| <= r );