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

( ( 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