let A be 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_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e
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_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e
let T be DivSequence of A; :: thesis: for e being Element of REAL st 0 < e & f | A is bounded_below holds
ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e
let e be Element of REAL ; :: thesis: ( 0 < e & f | A is bounded_below implies ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e )
assume AS: ( 0 < e & f | A is bounded_below ) ; :: thesis: ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e
defpred S₁[ 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 & middle_sum f,z <= (lower_sum f,(T . $1)) + e ) );
A1: for x being Element of NAT ex y being Element of REAL * st S₁[x,y]

proof

let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S₁[x,y]
consider z being middle_volume of f,T . x such that
X1: middle_sum f,z <= (lower_sum f,(T . x)) + e by PX0203, AS;
reconsider y = z as Element of REAL * by FINSEQ_1:def 11;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by X1; :: thesis: verum

end;

consider F being Function of NAT ,(REAL * ) such that
A2: for x being Element of NAT holds S₁[x,F . x] from FUNCT_2:sch 10(A1);
reconsider F = F as middle_volume_Sequence of f,T by A2, defx2;

now

let x be Element of NAT ; :: thesis: (middle_sum f,F) . x <= ((lower_sum f,T) . x) + e
ex z being middle_volume of f,T . x st
( z = F . x & middle_sum f,z <= (lower_sum f,(T . x)) + e ) by A2;
then (middle_sum f,F) . x <= (lower_sum f,(T . x)) + e by defx3;
hence (middle_sum f,F) . x <= ((lower_sum f,T) . x) + e by INTEGRA2:def 5; :: thesis: verum

end;

hence ex S being middle_volume_Sequence of f,T st
for i being Element of NAT holds (middle_sum f,S) . i <= ((lower_sum f,T) . i) + e ; :: thesis: verum