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_above & F2 is bounded_above holds
F1 + F2 is bounded_above
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_above & F2 is bounded_above holds
F1 + F2 is bounded_above
let F1 be Function of X,Y; :: thesis: for F2 being Function of X,Z st F1 is bounded_above & F2 is bounded_above holds
F1 + F2 is bounded_above
let F2 be Function of X,Z; :: thesis: ( F1 is bounded_above & F2 is bounded_above implies F1 + F2 is bounded_above )
assume that
A1: F1 is bounded_above and
A2: F2 is bounded_above ; :: thesis: F1 + F2 is bounded_above
A3: not sup F2 = +infty by A2, Def11;
A4: ( sup F1 in REAL & sup F2 in REAL implies (sup F1) + (sup F2) < +infty )

proof

reconsider a = sup F1, b = sup F2 as R_eal ;
assume that
A5: sup F1 in REAL and
A6: sup F2 in REAL ; :: thesis: (sup F1) + (sup F2) < +infty
reconsider a = a, b = b as Real by A5, A6;
(sup F1) + (sup F2) = a + b by XXREAL_3:def 2;
hence (sup F1) + (sup F2) < +infty by XXREAL_0:9; :: thesis: verum

end;

A7: ( sup F1 in REAL & sup F2 = -infty implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def 2;
A8: ( sup F1 = -infty & sup F2 = -infty implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def 2;
A9: ( sup F1 = -infty & sup F2 in REAL implies (sup F1) + (sup F2) < +infty ) by XXREAL_0:7, XXREAL_3:def 2;
A10: not sup F1 = +infty by A1, Def11;
sup (F1 + F2) < +infty

proof

assume not sup (F1 + F2) < +infty ; :: thesis: contradiction
then ( not sup (F1 + F2) <= +infty or sup (F1 + F2) = +infty ) by XXREAL_0:1;
hence contradiction by A10, A3, A4, A7, A9, A8, Th35, XXREAL_0:4, XXREAL_3:def 1; :: thesis: verum

end;

hence F1 + F2 is bounded_above by Def11; :: thesis: verum