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

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