let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL
for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

let f be Function of A,REAL; :: thesis: for T being DivSequence of A
for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

let T be DivSequence of A; :: thesis: for e being Element of REAL st 0 < e & f | A is bounded_above holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

let e be Element of REAL ; :: thesis: ( 0 < e & f | A is bounded_above implies ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i )

defpred S1[ Element of NAT , set ] means ( \$2 is middle_volume of f,T . \$1 & ex z being middle_volume of f,T . \$1 st
( z = \$2 & (upper_sum (f,(T . \$1))) - e <= middle_sum (f,z) ) );
assume A1: ( 0 < e & f | A is bounded_above ) ; :: thesis: ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i

A2: for x being Element of NAT ex y being Element of REAL * st S1[x,y]
proof
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S1[x,y]
consider z being middle_volume of f,T . x such that
A3: (upper_sum (f,(T . x))) - e <= middle_sum (f,z) by ;
reconsider y = z as Element of REAL * by FINSEQ_1:def 11;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by A3; :: thesis: verum
end;
consider F being sequence of () such that
A4: for x being Element of NAT holds S1[x,F . x] from reconsider F = F as middle_volume_Sequence of f,T by ;
now :: thesis: for x being Element of NAT holds ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x
let x be Element of NAT ; :: thesis: ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x
ex z being middle_volume of f,T . x st
( z = F . x & (upper_sum (f,(T . x))) - e <= middle_sum (f,z) ) by A4;
then (upper_sum (f,(T . x))) - e <= (middle_sum (f,F)) . x by Def4;
hence ((upper_sum (f,T)) . x) - e <= (middle_sum (f,F)) . x by INTEGRA2:def 2; :: thesis: verum
end;
hence ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds ((upper_sum (f,T)) . i) - e <= (middle_sum (f,S)) . i ; :: thesis: verum