let X, Y be set ; :: thesis: for f being real-valued Function st f | X is bounded_above & f | Y is bounded_above holds
f | (X \/ Y) is bounded_above
let f be real-valued Function; :: thesis: ( f | X is bounded_above & f | Y is bounded_above implies f | (X \/ Y) is bounded_above )
assume that
A1: f | X is bounded_above and
A2: f | Y is bounded_above ; :: thesis: f | (X \/ Y) is bounded_above
consider r1 being real number such that
A3: for c being set st c in X /\ (dom f) holds
f . c <= r1 by A1, Th87;
consider r2 being real number such that
A4: for c being set st c in Y /\ (dom f) holds
f . c <= r2 by A2, Th87;

now

take r = (abs r1) + (abs r2); :: thesis: for c being set st c in (X \/ Y) /\ (dom f) holds
f . c <= r
let c be set ; :: thesis: ( c in (X \/ Y) /\ (dom f) implies f . c <= r )
assume A5: c in (X \/ Y) /\ (dom f) ; :: thesis: f . c <= r
then A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by A5, XBOOLE_0:def 4;

now

per cases ( c in X or c in Y ) by A7, XBOOLE_0:def 3;

suppose c in X ; :: thesis: f . c <= r

then c in X /\ (dom f) by A6, XBOOLE_0:def 4;
then A8: f . c <= r1 by A3;
A9: 0 <= abs r2 by COMPLEX1:46;
r1 <= abs r1 by ABSVALUE:4;
then f . c <= abs r1 by A8, XXREAL_0:2;
then (f . c) + 0 <= r by A9, XREAL_1:7;
hence f . c <= r ; :: thesis: verum

end;

suppose c in Y ; :: thesis: f . c <= r

then c in Y /\ (dom f) by A6, XBOOLE_0:def 4;
then A10: f . c <= r2 by A4;
A11: 0 <= abs r1 by COMPLEX1:46;
r2 <= abs r2 by ABSVALUE:4;
then f . c <= abs r2 by A10, XXREAL_0:2;
then 0 + (f . c) <= r by A11, XREAL_1:7;
hence f . c <= r ; :: thesis: verum

end;

end;

end;

hence f . c <= r ; :: thesis: verum

end;

hence f | (X \/ Y) is bounded_above by Th87; :: thesis: verum