let A be non empty 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) ) )
consider g being Function of A,REAL such that
A1: rng g = {(lower_bound (rng f))} and
A2: g | A is bounded by Th5;
consider h being Function of A,REAL such that
A3: rng h = {(upper_bound (rng f))} and
A4: h | A is bounded by Th5;
A5: integral g = (lower_bound (rng f)) * (vol A) by A1, Th4;
assume A6: 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) ) )
A7: 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 x in dom f ; :: thesis: ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) )
then A8: f . x in rng f by FUNCT_1:def 3;
A9: rng f is bounded_below by A6, INTEGRA1:11;
rng f is bounded_above by A6, INTEGRA1:13;
hence ( lower_bound (rng f) <= f . x & f . x <= upper_bound (rng f) ) by A9, A8, SEQ_4:def 1, SEQ_4:def 2; :: thesis: verum

end;

A10: 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 A11: x in A ; :: thesis: f . x <= h . x
dom h = A by FUNCT_2:def 1;
then A12: h . x in rng h by A11, FUNCT_1:def 3;
dom f = A by FUNCT_2:def 1;
then f . x <= upper_bound (rng f) by A7, A11;
hence f . x <= h . x by A3, A12, TARSKI:def 1; :: thesis: verum

end;

A13: 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 A14: x in A ; :: thesis: g . x <= f . x
dom g = A by FUNCT_2:def 1;
then A15: g . x in rng g by A14, FUNCT_1:def 3;
dom f = A by FUNCT_2:def 1;
then lower_bound (rng f) <= f . x by A7, A14;
hence g . x <= f . x by A1, A15, TARSKI:def 1; :: thesis: verum

end;

assume A16: f is integrable ; :: thesis: ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) )
A17: integral h = (upper_bound (rng f)) * (vol A) by A3, Th4;
A18: h is integrable by A3, Th4;
A19: g is integrable by A1, Th4;

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

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

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

reconsider a = (integral f) / (vol A) as Real ;
A21: integral f = a * (vol A) by A20, XCMPLX_1:87;
A22: vol A >= 0 by INTEGRA1:9;
then A23: (integral f) / (vol A) <= upper_bound (rng f) by A6, A16, A4, A18, A17, A10, A20, INTEGRA2:34, XREAL_1:79;
lower_bound (rng f) <= (integral f) / (vol A) by A6, A16, A2, A19, A5, A13, A20, A22, INTEGRA2:34, XREAL_1:77;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A23, A21; :: thesis: verum

end;

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

A25: lower_bound (rng f) <= upper_bound (rng f)

proof

dom f = A by FUNCT_2:def 1;
then consider x being Element of REAL such that
A26: x in dom f by SUBSET_1:4;
A27: f . x <= upper_bound (rng f) by A7, A26;
lower_bound (rng f) <= f . x by A7, A26;
hence lower_bound (rng f) <= upper_bound (rng f) by A27, XXREAL_0:2; :: thesis: verum

end;

integral f = (lower_bound (rng f)) * (vol A) by A24, Th6;
hence ex a being Real st
( lower_bound (rng f) <= a & a <= upper_bound (rng f) & integral f = a * (vol A) ) by A25; :: 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