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 (lower_sum_set f) is bounded_above
let f be Function of A,REAL; :: thesis: ( f | A is bounded implies rng (lower_sum_set f) is bounded_above )
set D1 = the Division of A;
assume A1: f | A is bounded ; :: thesis: rng (lower_sum_set f) is bounded_above
take upper_sum (f, the Division of A) ; :: according to XXREAL_2:def 10 :: thesis: upper_sum (f, the Division of A) is UpperBound of rng (lower_sum_set f)
let a be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not a in rng (lower_sum_set f) or a <= upper_sum (f, the Division of A) )
assume a in rng (lower_sum_set f) ; :: thesis: a <= upper_sum (f, the Division of A)
then consider D being Element of divs A such that
A2: ( D in dom (lower_sum_set f) & a = (lower_sum_set f) . D ) by PARTFUN1:3;
reconsider D = D as Division of A by INTEGRA1:def 3;
a = lower_sum (f,D) by A2, INTEGRA1:def 11;
hence a <= upper_sum (f, the Division of A) by A1, INTEGRA1:48; :: thesis: verum