:: deftheorem defines is_bounded_on VFUNCT_2:def 3 :
for M being non empty set
for V being ComplexNormSpace
for f being PartFunc of M,V
for Y being set holds
( f is_bounded_on Y iff ex r being Real st
for x being Element of M st x in Y /\ (dom f) holds
||.(f /. x).|| <= r );