let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
let f be Function of A,REAL ; :: thesis: ( f | A is bounded & f is integrable implies ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) )
assume A1: f | A is bounded ; :: thesis: ( not f is integrable or ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) )
assume A2: f is integrable ; :: thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
A3: for x being Real st x in dom f holds
( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) )

proof

let x be Real; :: thesis: ( x in dom f implies ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) )
assume A4: x in dom f ; :: thesis: ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) )
( f | A is bounded_above & f | A is bounded_below ) by A1;
then A5: ( rng f is bounded_above & rng f is bounded_below ) by INTEGRA1:13, INTEGRA1:15;
f . x in rng f by A4, FUNCT_1:def 5;
hence ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) by A5, SEQ_4:def 4, SEQ_4:def 5; :: thesis: verum

end;

consider g being Function of A,REAL such that
A6: ( rng g = {(lower_bound (rng f))} & g | A is bounded ) by Th5;
A7: ( g is integrable & integral g = (lower_bound (rng f)) * (vol A) ) by A6, Th4;
consider h being Function of A,REAL such that
A8: ( rng h = {(upper_bound (rng f))} & h | A is bounded ) by Th5;
A9: ( h is integrable & integral h = (upper_bound (rng f)) * (vol A) ) by A8, Th4;
A10: for x being Real st x in A holds
g . x <= f . x

proof

let x be Real; :: thesis: ( x in A implies g . x <= f . x )
assume A11: x in A ; :: thesis: g . x <= f . x
dom f = A by FUNCT_2:def 1;
then A12: lower_bound (rng f) <= f . x by A3, A11;
dom g = A by FUNCT_2:def 1;
then g . x in rng g by A11, FUNCT_1:def 5;
hence g . x <= f . x by A6, A12, TARSKI:def 1; :: thesis: verum

end;

for x being Real st x in A holds
f . x <= h . x

proof

let x be Real; :: thesis: ( x in A implies f . x <= h . x )
assume A13: x in A ; :: thesis: f . x <= h . x
dom f = A by FUNCT_2:def 1;
then A14: f . x <= upper_bound (rng f) by A3, A13;
dom h = A by FUNCT_2:def 1;
then h . x in rng h by A13, FUNCT_1:def 5;
hence f . x <= h . x by A8, A14, TARSKI:def 1; :: thesis: verum

end;

then A15: ( (lower_bound (rng f)) * (vol A) <= integral f & integral f <= (upper_bound (rng f)) * (vol A) ) by A1, A2, A6, A7, A8, A9, A10, INTEGRA2:34;

now

per cases ( vol A <> 0 or vol A = 0 ) ;

suppose A16: vol A <> 0 ; :: thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )

vol A >= 0 by INTEGRA1:11;
then A17: ( lower_bound (rng f) <= (integral f) / (vol A) & (integral f) / (vol A) <= upper_bound (rng f) ) by A15, A16, XREAL_1:79, XREAL_1:81;
reconsider a = (integral f) / (vol A) as Real ;
integral f = a * (vol A) by A16, XCMPLX_1:88;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A17; :: thesis: verum

end;

suppose vol A = 0 ; :: thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )

then A18: integral f = (lower_bound (rng f)) * (vol A) by Th6;
lower_bound (rng f) <= upper_bound (rng f)

proof

dom f = A by FUNCT_2:def 1;
then consider x being Real such that
A19: x in dom f by SUBSET_1:10;
( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) by A3, A19;
hence lower_bound (rng f) <= upper_bound (rng f) by XXREAL_0:2; :: thesis: verum

end;

hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A18; :: thesis: verum

end;

end;

end;

hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) ; :: thesis: verum