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₁[ 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₁[x,y] consider F being sequence of (REAL *) such that
A4: for x being Element of NAT holds S₁[x,F . x] from FUNCT_2:sch 3(A2);
reconsider F = F as middle_volume_Sequence of f,T by A4, Def3;
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