for X, Y being set
for C being non empty set
for f1, f2 being PartFunc of C,REAL holds
( ( f1 | X is bounded_above & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_above ) & ( f1 | X is bounded_below & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded_below ) & ( f1 | X is bounded & f2 | Y is constant implies (f1 + f2) | (X /\ Y) is bounded ) ) by Th83;