for M being non empty set
for V being ComplexNormSpace
for f1, f2 being PartFunc of M,V
for X, Y being set st f1 is_bounded_on X & f2 | Y is constant holds
f1 + f2 is_bounded_on X /\ Y