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 A1: ( f | X is bounded & f | Y is bounded ) ; :: thesis: f | (X \/ Y) is bounded
thus f | (X \/ Y) is bounded_above by A1, Th102; :: according to SEQ_2:def 8 :: thesis: f | (X \/ Y) is bounded_below
thus f | (X \/ Y) is bounded_below by A1, Th103; :: thesis: verum