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 A1, Th71;

consider r2 being Real such that

A4: for c being object st c in Y /\ (dom f) holds

r2 <= f . c by A2, Th71;

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 A1, Th71;

consider r2 being Real such that

A4: for c being object st c in Y /\ (dom f) holds

r2 <= f . c by A2, Th71;

now :: thesis: ex r being set st

for c being object st c in (X \/ Y) /\ (dom f) holds

r <= f . c

hence
f | (X \/ Y) is bounded_below
by Th71; :: thesis: verumfor 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 A5, XBOOLE_0:def 4;

end;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 A5, XBOOLE_0:def 4;

now :: thesis: r <= f . cend;

hence
r <= f . c
; :: thesis: verumper cases
( c in X or c in Y )
by A7, XBOOLE_0:def 3;

end;

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

then
c in X /\ (dom f)
by A6, XBOOLE_0:def 4;

then A8: r1 <= f . c by A3;

A9: 0 <= |.r2.| by COMPLEX1:46;

- |.r1.| <= r1 by ABSVALUE:4;

then - |.r1.| <= f . c by A8, XXREAL_0:2;

then r <= (f . c) - 0 by A9, XREAL_1:13;

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

end;then A8: r1 <= f . c by A3;

A9: 0 <= |.r2.| by COMPLEX1:46;

- |.r1.| <= r1 by ABSVALUE:4;

then - |.r1.| <= f . c by A8, XXREAL_0:2;

then r <= (f . c) - 0 by A9, XREAL_1:13;

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

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

then
c in Y /\ (dom f)
by A6, XBOOLE_0:def 4;

then A10: r2 <= f . c by A4;

A11: 0 <= |.r1.| by COMPLEX1:46;

- |.r2.| <= r2 by ABSVALUE:4;

then - |.r2.| <= f . c by A10, XXREAL_0:2;

then (- |.r2.|) - |.r1.| <= (f . c) - 0 by A11, XREAL_1:13;

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

end;then A10: r2 <= f . c by A4;

A11: 0 <= |.r1.| by COMPLEX1:46;

- |.r2.| <= r2 by ABSVALUE:4;

then - |.r2.| <= f . c by A10, XXREAL_0:2;

then (- |.r2.|) - |.r1.| <= (f . c) - 0 by A11, XREAL_1:13;

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