let X, Y be set ; :: thesis: for f1, f2 being real-valued Function holds
( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
let f1, f2 be real-valued Function; :: thesis: ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) )
(f1 + f2) | (X /\ Y) = (f1 | (X /\ Y)) + (f2 | (X /\ Y)) by Th44
.= (f1 | (X /\ Y)) + ((f2 | Y) | X) by RELAT_1:71
.= ((f1 | X) | Y) + ((f2 | Y) | X) by RELAT_1:71 ;
hence ( ( f1 | X is bounded_above & f2 | Y is bounded_above implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is bounded_below implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is bounded implies (f1 + f2) | (X /\ Y) is bounded ) ) ; :: thesis: verum