theorem Th83: :: RFUNCT_1:83

for X, Y being set
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 ) )