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_below & F2 is bounded_below holds

F1 + F2 is bounded_below

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_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 that

A1: F1 is bounded_below and

A2: F2 is bounded_below ; :: thesis: F1 + F2 is bounded_below

A4: ( inf F1 in REAL & inf F2 in REAL implies -infty < (inf F1) + (inf F2) )

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

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

-infty < inf (F1 + F2)

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: 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 that

A1: F1 is bounded_below and

A2: F2 is bounded_below ; :: thesis: F1 + F2 is bounded_below

A4: ( inf F1 in REAL & inf F2 in REAL implies -infty < (inf F1) + (inf F2) )

proof

A7:
( inf F1 in REAL & inf F2 = +infty implies -infty < (inf F1) + (inf F2) )
by XXREAL_0:7, XXREAL_3:def 2;
reconsider a = inf F1, b = inf F2 as R_eal ;

assume that

A5: inf F1 in REAL and

A6: inf F2 in REAL ; :: thesis: -infty < (inf F1) + (inf F2)

reconsider a = a, b = b as Element of REAL by A5, A6;

(inf F1) + (inf F2) = a + b by XXREAL_3:def 2;

hence -infty < (inf F1) + (inf F2) by XXREAL_0:12; :: thesis: verum

end;assume that

A5: inf F1 in REAL and

A6: inf F2 in REAL ; :: thesis: -infty < (inf F1) + (inf F2)

reconsider a = a, b = b as Element of REAL by A5, A6;

(inf F1) + (inf F2) = a + b by XXREAL_3:def 2;

hence -infty < (inf F1) + (inf F2) by XXREAL_0:12; :: thesis: verum

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

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

-infty < inf (F1 + F2)

proof

hence
F1 + F2 is bounded_below
; :: thesis: verum
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 A1, A2, A4, A7, A9, A8, Th17, XXREAL_0:6, XXREAL_3:def 1; :: thesis: verum

end;then ( not -infty <= inf (F1 + F2) or inf (F1 + F2) = -infty ) by XXREAL_0:1;

hence contradiction by A1, A2, A4, A7, A9, A8, Th17, XXREAL_0:6, XXREAL_3:def 1; :: thesis: verum