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_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F
let f be Function of A,REAL ; :: thesis: for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F
let D be Division of A; :: thesis: for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F
let e be Real; :: thesis: ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F )
A1: 0 < len D by FINSEQ_1:28;
len (upper_volume f,D) = len D by INTEGRA1:def 7;
then reconsider p = upper_volume f,D as Element of (len D) -tuples_on REAL by FINSEQ_2:110;
set e1 = e / (len D);
assume ( f | A is bounded_above & 0 < e ) ; :: thesis: ex F being middle_volume of f,D st (upper_sum f,D) - e <= middle_sum f,F
then consider F being middle_volume of f,D such that
A2: for i being Nat st i in dom D holds
( F . i <= (upper_volume f,D) . i & ((upper_volume f,D) . i) - (e / (len D)) < F . i ) by A1, Lm3, XREAL_1:141;
set s = (len D) |-> (e / (len D));
reconsider t = p - ((len D) |-> (e / (len D))) as Element of (len D) -tuples_on REAL ;
take F ; :: thesis: (upper_sum f,D) - e <= middle_sum f,F
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:110;

now

let i be Nat; :: thesis: ( i in Seg (len D) implies t . i <= q . i )
assume A3: i in Seg (len D) ; :: thesis: t . i <= q . i
then i in dom D by FINSEQ_1:def 3;
then (p . i) - (e / (len D)) <= q . i by A2;
then (p . i) - (((len D) |-> (e / (len D))) . i) <= q . i by A3, FINSEQ_2:71;
hence t . i <= q . i by RVSUM_1:48; :: thesis: verum

end;

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