let X, Y be set ; :: thesis: for f being real-valued Function st f | X is bounded & f | Y is bounded holds
f | (X \/ Y) is bounded
let f be real-valued Function; :: thesis: ( f | X is bounded & f | Y is bounded implies f | (X \/ Y) is bounded )
assume that
A1: f | X is bounded and
A2: f | Y is bounded ; :: thesis: f | (X \/ Y) is bounded
thus f | (X \/ Y) is bounded_above by A1, A2, Th102; :: according to SEQ_2:def 8 :: thesis: f | (X \/ Y) is bounded_below
thus f | (X \/ Y) is bounded_below by A1, A2, Th103; :: thesis: verum