let X be set ; :: thesis: for C being non empty set
for V being RealNormSpace
for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let C be non empty set ; :: thesis: for V being RealNormSpace
for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let V be RealNormSpace; :: thesis: for f being PartFunc of C,V st X misses dom f holds
f is_bounded_on X
let f be PartFunc of C,V; :: 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 c being Element of C st c in X /\ (dom f) holds
||.(f /. c).|| <= 0 ;
hence f is_bounded_on X ; :: thesis: verum