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_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 )

defpred S_{1}[ 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 ) );

assume A1: ( 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

A2: for x being Element of NAT ex y being Element of REAL * st S_{1}[x,y]

A4: for x being Element of NAT holds S_{1}[x,F . x]
from FUNCT_2:sch 3(A2);

reconsider F = F as middle_volume_Sequence of f,T by A4, Def3;

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

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 )

defpred S

( z = $2 & middle_sum (f,z) <= (lower_sum (f,(T . $1))) + e ) );

assume A1: ( 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

A2: for x being Element of NAT ex y being Element of REAL * st S

proof

consider F being sequence of (REAL *) such that
let x be Element of NAT ; :: thesis: ex y being Element of REAL * st S_{1}[x,y]

consider z being middle_volume of f,T . x such that

A3: middle_sum (f,z) <= (lower_sum (f,(T . x))) + e by A1, Th3;

reconsider y = z as Element of REAL * by FINSEQ_1:def 11;

take y ; :: thesis: S_{1}[x,y]

thus S_{1}[x,y]
by A3; :: thesis: verum

end;consider z being middle_volume of f,T . x such that

A3: middle_sum (f,z) <= (lower_sum (f,(T . x))) + e by A1, Th3;

reconsider y = z as Element of REAL * by FINSEQ_1:def 11;

take y ; :: thesis: S

thus S

A4: for x being Element of NAT holds S

reconsider F = F as middle_volume_Sequence of f,T by A4, Def3;

now :: thesis: for x being Element of NAT holds (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e

hence
ex S being middle_volume_Sequence of f,T st 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 A4;

then (middle_sum (f,F)) . x <= (lower_sum (f,(T . x))) + e by Def4;

hence (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e by INTEGRA2:def 3; :: thesis: verum

end;ex z being middle_volume of f,T . x st

( z = F . x & middle_sum (f,z) <= (lower_sum (f,(T . x))) + e ) by A4;

then (middle_sum (f,F)) . x <= (lower_sum (f,(T . x))) + e by Def4;

hence (middle_sum (f,F)) . x <= ((lower_sum (f,T)) . x) + e by INTEGRA2:def 3; :: thesis: verum

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