let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum f,T) . i <= (middle_sum f,S) . i
let f be Function of A,REAL ; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum f,T) . i <= (middle_sum f,S) . i
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T
for i being Element of NAT st f | A is bounded_below holds
(lower_sum f,T) . i <= (middle_sum f,S) . i
let S be middle_volume_Sequence of f,T; :: thesis: for i being Element of NAT st f | A is bounded_below holds
(lower_sum f,T) . i <= (middle_sum f,S) . i
let i be Element of NAT ; :: thesis: ( f | A is bounded_below implies (lower_sum f,T) . i <= (middle_sum f,S) . i )
assume AS: f | A is bounded_below ; :: thesis: (lower_sum f,T) . i <= (middle_sum f,S) . i
P1: (middle_sum f,S) . i = middle_sum f,(S . i) by defx3;
(lower_sum f,T) . i = lower_sum f,(T . i) by INTEGRA2:def 5;
hence (lower_sum f,T) . i <= (middle_sum f,S) . i by AS, PX0103, P1; :: thesis: verum