let X be set ; :: thesis: for C being non empty set
for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
let C be non empty set ; :: thesis: for f being PartFunc of C,COMPLEX st X misses dom f holds
f | X is bounded
let f be PartFunc of C,COMPLEX; :: thesis: ( X misses dom f implies f | X is bounded )
assume X /\ (dom f) = {} ; :: according to XBOOLE_0:def 7 :: thesis: f | X is bounded
then for c being Element of C st c in X /\ (dom f) holds
|.(f /. c).| <= 0 ;
hence f | X is bounded by Th68; :: thesis: verum