let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let f be Function of A,REAL; :: thesis: for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let D be Division of A; :: thesis: for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let e be Real; :: thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e )

len (lower_volume (f,D)) = len D by INTEGRA1:def 7;

then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

reconsider e1 = e / (len D) as Element of REAL by XREAL_0:def 1;

assume ( f | A is bounded_below & 0 < e ) ; :: thesis: ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

then consider F being middle_volume of f,D such that

A1: for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e1 ) by Lm2, XREAL_1:139;

set s = (len D) |-> e1;

reconsider t = p + ((len D) |-> e1) as Element of (len D) -tuples_on REAL ;

take F ; :: thesis: middle_sum (f,F) <= (lower_sum (f,D)) + e

len F = len D by Def1;

then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

then Sum q <= (Sum p) + (Sum ((len D) |-> e1)) by RVSUM_1:89;

then Sum q <= (Sum p) + ((len D) * e1) by RVSUM_1:80;

hence middle_sum (f,F) <= (lower_sum (f,D)) + e by XCMPLX_1:87; :: thesis: verum

for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let f be Function of A,REAL; :: thesis: for D being Division of A

for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let D be Division of A; :: thesis: for e being Real st f | A is bounded_below & 0 < e holds

ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

let e be Real; :: thesis: ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e )

len (lower_volume (f,D)) = len D by INTEGRA1:def 7;

then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

reconsider e1 = e / (len D) as Element of REAL by XREAL_0:def 1;

assume ( f | A is bounded_below & 0 < e ) ; :: thesis: ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e

then consider F being middle_volume of f,D such that

A1: for i being Nat st i in dom D holds

( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e1 ) by Lm2, XREAL_1:139;

set s = (len D) |-> e1;

reconsider t = p + ((len D) |-> e1) as Element of (len D) -tuples_on REAL ;

take F ; :: thesis: middle_sum (f,F) <= (lower_sum (f,D)) + e

len F = len D by Def1;

then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

now :: thesis: for i being Nat st i in Seg (len D) holds

q . i <= t . i

then
Sum q <= Sum t
by RVSUM_1:82;q . i <= t . i

let i be Nat; :: thesis: ( i in Seg (len D) implies q . i <= t . i )

assume A2: i in Seg (len D) ; :: thesis: q . i <= t . i

then i in dom D by FINSEQ_1:def 3;

then q . i <= (p . i) + e1 by A1;

then q . i <= (p . i) + (((len D) |-> e1) . i) by A2, FINSEQ_2:57;

hence q . i <= t . i by RVSUM_1:11; :: thesis: verum

end;assume A2: i in Seg (len D) ; :: thesis: q . i <= t . i

then i in dom D by FINSEQ_1:def 3;

then q . i <= (p . i) + e1 by A1;

then q . i <= (p . i) + (((len D) |-> e1) . i) by A2, FINSEQ_2:57;

hence q . i <= t . i by RVSUM_1:11; :: thesis: verum

then Sum q <= (Sum p) + (Sum ((len D) |-> e1)) by RVSUM_1:89;

then Sum q <= (Sum p) + ((len D) * e1) by RVSUM_1:80;

hence middle_sum (f,F) <= (lower_sum (f,D)) + e by XCMPLX_1:87; :: thesis: verum