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

now

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

now

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

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

then c in X /\ (dom f) by A4, XBOOLE_0:def 4;
then A5: r1 <= f . c by A2;
- (abs r1) <= r1 by ABSVALUE:11;
then A6: - (abs r1) <= f . c by A5, XXREAL_0:2;
0 <= abs r2 by COMPLEX1:132;
then r <= (f . c) - 0 by A6, XREAL_1:15;
hence r <= f . c ; :: thesis: verum

end;

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

then c in Y /\ (dom f) by A4, XBOOLE_0:def 4;
then A7: r2 <= f . c by A3;
- (abs r2) <= r2 by ABSVALUE:11;
then A8: - (abs r2) <= f . c by A7, XXREAL_0:2;
0 <= abs r1 by COMPLEX1:132;
then (- (abs r2)) - (abs r1) <= (f . c) - 0 by A8, XREAL_1:15;
hence r <= f . c ; :: thesis: verum

end;

end;

end;

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

end;

hence f | (X \/ Y) is bounded_below by Def10; :: thesis: verum