let X be set ; :: thesis: for f being real-valued Function st X misses dom f holds
f | X is bounded
let f be real-valued Function; :: 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 dom (f | X) = {} by RELAT_1:61;
then f | X = {} ;
hence f | X is bounded ; :: thesis: verum