let X be non empty set ; :: thesis: for Y, Z being non empty Subset of ExtREAL
for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let Y, Z be non empty Subset of ExtREAL; :: thesis: for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let F1 be Function of X,Y; :: thesis: for F2 being Function of X,Z st F1 is bounded & F2 is bounded holds
F1 + F2 is bounded
let F2 be Function of X,Z; :: thesis: ( F1 is bounded & F2 is bounded implies F1 + F2 is bounded )
assume that
A1: F1 is bounded and
A2: F2 is bounded ; :: thesis: F1 + F2 is bounded
A3: F1 + F2 is bounded_below by A1, A2, Th50;
F1 + F2 is bounded_above by A1, A2, Th49;
hence F1 + F2 is bounded by A3; :: thesis: verum