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 such that

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

f . c <= r1 by A1, Th70;

consider r2 being Real such that

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

f . c <= r2 by A2, Th70;

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 such that

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

f . c <= r1 by A1, Th70;

consider r2 being Real such that

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

f . c <= r2 by A2, Th70;

now :: thesis: ex r being set st

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

f . c <= r

hence
f | (X \/ Y) is bounded_above
by Th70; :: thesis: verumfor c being object st c in (X \/ Y) /\ (dom f) holds

f . c <= r

take r = |.r1.| + |.r2.|; :: thesis: for c being object st c in (X \/ Y) /\ (dom f) holds

f . c <= r

let c be object ; :: 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;

end;f . c <= r

let c be object ; :: 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 :: thesis: f . c <= rend;

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

end;