let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL
for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let f be Function of A,REAL; :: thesis: for D being Division of A
for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let D be Division of A; :: thesis: for F being middle_volume of f,D st f | A is bounded_below holds
lower_sum (f,D) <= middle_sum (f,F)
let F be middle_volume of f,D; :: thesis: ( f | A is bounded_below implies lower_sum (f,D) <= middle_sum (f,F) )
len (lower_volume (f,D)) = len D by INTEGRA1:def 7;
then reconsider p = lower_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
len F = len D by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
assume A1: f | A is bounded_below ; :: thesis: lower_sum (f,D) <= middle_sum (f,F)

now :: thesis: for i being Nat st i in Seg (len D) holds
p . i <= q . i

let i be Nat; :: thesis: ( i in Seg (len D) implies p . i <= q . i )
assume i in Seg (len D) ; :: thesis: p . i <= q . i
then i in dom D by FINSEQ_1:def 3;
hence p . i <= q . i by A1, Lm1; :: thesis: verum

end;

hence lower_sum (f,D) <= middle_sum (f,F) by RVSUM_1:82; :: thesis: verum