let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded holds
( f is upper_integrable & f is lower_integrable )
let f be Function of A,REAL ; :: thesis: ( f | A is bounded implies ( f is upper_integrable & f is lower_integrable ) )
assume A1: f | A is bounded ; :: thesis: ( f is upper_integrable & f is lower_integrable )
for r being real number st r in rng (upper_sum_set f) holds
(lower_bound (rng f)) * (vol A) <= r

proof

let r be real number ; :: thesis: ( r in rng (upper_sum_set f) implies (lower_bound (rng f)) * (vol A) <= r )
assume r in rng (upper_sum_set f) ; :: thesis: (lower_bound (rng f)) * (vol A) <= r
then consider D being Element of divs A such that
A2: D in dom (upper_sum_set f) and
A3: (upper_sum_set f) . D = r by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = upper_sum f,D by A2, A3, INTEGRA1:def 11;
then A4: lower_sum f,D <= r by A1, INTEGRA1:30;
(lower_bound (rng f)) * (vol A) <= lower_sum f,D by A1, INTEGRA1:27;
hence (lower_bound (rng f)) * (vol A) <= r by A4, XXREAL_0:2; :: thesis: verum

end;

then rng (upper_sum_set f) is bounded_below by SEQ_4:def 2;
hence f is upper_integrable by INTEGRA1:def 13; :: thesis: f is lower_integrable
for r being real number st r in rng (lower_sum_set f) holds
(upper_bound (rng f)) * (vol A) >= r

proof

let r be real number ; :: thesis: ( r in rng (lower_sum_set f) implies (upper_bound (rng f)) * (vol A) >= r )
assume r in rng (lower_sum_set f) ; :: thesis: (upper_bound (rng f)) * (vol A) >= r
then consider D being Element of divs A such that
A5: D in dom (lower_sum_set f) and
A6: (lower_sum_set f) . D = r by PARTFUN1:26;
reconsider D = D as Division of A by INTEGRA1:def 3;
r = lower_sum f,D by A5, A6, INTEGRA1:def 12;
then A7: upper_sum f,D >= r by A1, INTEGRA1:30;
(upper_bound (rng f)) * (vol A) >= upper_sum f,D by A1, INTEGRA1:29;
hence (upper_bound (rng f)) * (vol A) >= r by A7, XXREAL_0:2; :: thesis: verum

end;

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