let A be 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 )
assume AS: ( 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
P1: 0 < len D by FINSEQ_1:28;
set e1 = e / (len D);
consider F being middle_volume of f,D such that
R1: for i being Nat st i in dom D holds
( (lower_volume f,D) . i <= F . i & F . i < ((lower_volume f,D) . i) + (e / (len D)) ) by AS, P1, PX0201, XREAL_1:141;
take F ; :: thesis: middle_sum f,F <= (lower_sum f,D) + e
set s = (len D) |-> (e / (len D));
A1: len (lower_volume f,D) = len D by INTEGRA1:def 8;
B1: len F = len D by defx0;
reconsider p = lower_volume f,D as Element of (len D) -tuples_on REAL by A1, FINSEQ_2:110;
reconsider q = F as Element of (len D) -tuples_on REAL by B1, FINSEQ_2:110;
reconsider t = p + ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ;

now

let i be Nat; :: thesis: ( i in Seg (len D) implies q . i <= t . i )
assume C0: 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) + (e / (len D)) by R1;
then q . i <= (p . i) + (((len D) |-> (e / (len D))) . i) by FINSEQ_2:71, C0;
hence q . i <= t . i by RVSUM_1:27; :: thesis: verum

end;

then Sum q <= Sum t by RVSUM_1:112;
then Sum q <= (Sum p) + (Sum ((len D) |-> (e / (len D)))) by RVSUM_1:119;
then Sum q <= (Sum p) + ((len D) * (e / (len D))) by RVSUM_1:110;
hence middle_sum f,F <= (lower_sum f,D) + e by XCMPLX_1:88, P1; :: thesis: verum