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 that
A1: f | X is bounded_below and
A2: f | Y is bounded_below ; :: thesis: f | (X \/ Y) is bounded_below
consider r1 being Real such that
A3: for c being object st c in X /\ (dom f) holds
r1 <= f . c by ;
consider r2 being Real such that
A4: for c being object st c in Y /\ (dom f) holds
r2 <= f . c by ;
now :: thesis: ex r being set st
for c being object st c in (X \/ Y) /\ (dom f) holds
r <= f . c
take r = (- |.r1.|) - |.r2.|; :: thesis: for c being object st c in (X \/ Y) /\ (dom f) holds
r <= f . c

let c be object ; :: thesis: ( c in (X \/ Y) /\ (dom f) implies r <= f . c )
assume A5: c in (X \/ Y) /\ (dom f) ; :: thesis: r <= f . c
then A6: c in dom f by XBOOLE_0:def 4;
A7: c in X \/ Y by ;
now :: thesis: r <= f . c
per cases ( c in X or c in Y ) by ;
suppose c in X ; :: thesis: r <= f . c
then c in X /\ (dom f) by ;
then A8: r1 <= f . c by A3;
A9: 0 <= |.r2.| by COMPLEX1:46;
- |.r1.| <= r1 by ABSVALUE:4;
then - |.r1.| <= f . c by ;
then r <= (f . c) - 0 by ;
hence r <= f . c ; :: thesis: verum
end;
suppose c in Y ; :: thesis: r <= f . c
then c in Y /\ (dom f) by ;
then A10: r2 <= f . c by A4;
A11: 0 <= |.r1.| by COMPLEX1:46;
- |.r2.| <= r2 by ABSVALUE:4;
then - |.r2.| <= f . c by ;
then (- |.r2.|) - |.r1.| <= (f . c) - 0 by ;
hence r <= f . c ; :: thesis: verum
end;
end;
end;
hence r <= f . c ; :: thesis: verum
end;
hence f | (X \/ Y) is bounded_below by Th71; :: thesis: verum