let A be 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 )
assume A1: f | A is bounded ; :: thesis: rng (lower_sum_set f) is bounded_above
consider D1 being Element of divs A;
for a being real number st a in rng (lower_sum_set f) holds
a <= upper_sum f,D1

proof

let a be real number ; :: thesis: ( a in rng (lower_sum_set f) implies a <= upper_sum f,D1 )
assume a in rng (lower_sum_set f) ; :: thesis: a <= upper_sum f,D1
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:26;
a = lower_sum f,D by A2, INTEGRA1:def 12;
hence a <= upper_sum f,D1 by A1, INTEGRA1:50; :: thesis: verum

end;

hence rng (lower_sum_set f) is bounded_above by SEQ_4:def 1; :: thesis: verum