let A be non empty closed_interval Subset of REAL; :: thesis:
let f be Function of A,REAL; :: thesis:
let D be Division of A; :: thesis:
let e be Real; :: thesis:
len (upper_volume (f,D)) = len D by INTEGRA1:def 6;
then reconsider p = upper_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_above & 0 < e ) ; :: thesis:
then consider F being middle_volume of f,D such that
A1: for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e1 < F . i ) by Lm3, 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:
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;

now :: thesis:

let i be Nat; :: thesis:
assume A2: i in Seg (len D) ; :: thesis:
then i in dom D by FINSEQ_1:def 3;
then (p . i) - e1 <= q . i by A1;
then (p . i) - (((len D) |-> e1) . i) <= q . i by A2, FINSEQ_2:57;
hence t . i <= q . i by RVSUM_1:27; :: thesis:

end;

then Sum t <= Sum q by RVSUM_1:82;
then (Sum p) - (Sum ((len D) |-> e1)) <= Sum q by RVSUM_1:90;
then (Sum p) - ((len D) * e1) <= Sum q by RVSUM_1:80;
hence (upper_sum (f,D)) - e <= middle_sum (f,F) by XCMPLX_1:87; :: thesis: