let M be non empty set ; :: thesis: for V being ComplexNormSpace
for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
let V be ComplexNormSpace; :: thesis: for f being PartFunc of M,V
for X being set st X misses dom f holds
f is_bounded_on X
let f be PartFunc of M,V; :: thesis: for X being set st X misses dom f holds
f is_bounded_on X
let X be set ; :: thesis: ( X misses dom f implies f is_bounded_on X )
assume X /\ (dom f) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f is_bounded_on X
then for x being Element of M st x in X /\ (dom f) holds
||.(f /. x).|| <= 0 ;
hence f is_bounded_on X ; :: thesis: verum