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 )
then A2: ( f | A is bounded_above & f | A is bounded_below ) ;
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
A3: ( D in dom (upper_sum_set f) & (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 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 A2, 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) & (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, INTEGRA1:def 12;
then A6: upper_sum f,D >= r by A1, INTEGRA1:30;
(upper_bound (rng f)) * (vol A) >= upper_sum f,D by A2, INTEGRA1:29;
hence (upper_bound (rng f)) * (vol A) >= r by A6, 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