let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded holds

rng (upper_sum_set f) is bounded_below

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies rng (upper_sum_set f) is bounded_below )

set D1 = the Division of A;

assume A1: f | A is bounded ; :: thesis: rng (upper_sum_set f) is bounded_below

take lower_sum (f, the Division of A) ; :: according to XXREAL_2:def 9 :: thesis: lower_sum (f, the Division of A) is LowerBound of rng (upper_sum_set f)

let a be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not a in rng (upper_sum_set f) or lower_sum (f, the Division of A) <= a )

assume a in rng (upper_sum_set f) ; :: thesis: lower_sum (f, the Division of A) <= a

then consider D being Element of divs A such that

A2: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:3;

reconsider D = D as Division of A by INTEGRA1:def 3;

a = upper_sum (f,D) by A2, INTEGRA1:def 10;

hence lower_sum (f, the Division of A) <= a by A1, INTEGRA1:48; :: thesis: verum

rng (upper_sum_set f) is bounded_below

let f be Function of A,REAL; :: thesis: ( f | A is bounded implies rng (upper_sum_set f) is bounded_below )

set D1 = the Division of A;

assume A1: f | A is bounded ; :: thesis: rng (upper_sum_set f) is bounded_below

take lower_sum (f, the Division of A) ; :: according to XXREAL_2:def 9 :: thesis: lower_sum (f, the Division of A) is LowerBound of rng (upper_sum_set f)

let a be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not a in rng (upper_sum_set f) or lower_sum (f, the Division of A) <= a )

assume a in rng (upper_sum_set f) ; :: thesis: lower_sum (f, the Division of A) <= a

then consider D being Element of divs A such that

A2: ( D in dom (upper_sum_set f) & a = (upper_sum_set f) . D ) by PARTFUN1:3;

reconsider D = D as Division of A by INTEGRA1:def 3;

a = upper_sum (f,D) by A2, INTEGRA1:def 10;

hence lower_sum (f, the Division of A) <= a by A1, INTEGRA1:48; :: thesis: verum