let X be non empty set ; :: thesis: for Y, Z being non empty Subset of ExtREAL st Y c= REAL & Z c= REAL holds
for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds
F1 + F2 is bounded_below
let Y, Z be non empty Subset of ExtREAL ; :: thesis: ( Y c= REAL & Z c= REAL implies for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds
F1 + F2 is bounded_below )
assume ( Y c= REAL & Z c= REAL ) ; :: thesis: for F1 being Function of X,Y
for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds
F1 + F2 is bounded_below
let F1 be Function of X,Y; :: thesis: for F2 being Function of X,Z st F1 is bounded_below & F2 is bounded_below holds
F1 + F2 is bounded_below
let F2 be Function of X,Z; :: thesis: ( F1 is bounded_below & F2 is bounded_below implies F1 + F2 is bounded_below )
assume A2: ( F1 is bounded_below & F2 is bounded_below ) ; :: thesis: F1 + F2 is bounded_below
A4: ( not inf F1 = -infty & not inf F2 = -infty ) by A2, Def12;
A5: ( inf F1 in REAL & inf F2 in REAL implies -infty < (inf F1) + (inf F2) )

proof

assume A6: ( inf F1 in REAL & inf F2 in REAL ) ; :: thesis: -infty < (inf F1) + (inf F2)
reconsider a = inf F1, b = inf F2 as R_eal ;
reconsider a = a, b = b as Real by A6;
(inf F1) + (inf F2) = a + b by Th1;
hence -infty < (inf F1) + (inf F2) by XXREAL_0:12; :: thesis: verum

end;

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

proof

assume inf (F1 + F2) <= -infty ; :: thesis: contradiction
then ( not -infty <= inf (F1 + F2) or inf (F1 + F2) = -infty ) by XXREAL_0:1;
hence contradiction by A4, A5, A7, A8, A9, Th36, XXREAL_0:6, XXREAL_3:def 1; :: thesis: verum

end;

hence F1 + F2 is bounded_below by Def12; :: thesis: verum