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_above holds

middle_sum (f,F) <= upper_sum (f,D)

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_above holds

middle_sum (f,F) <= upper_sum (f,D)

let D be Division of A; :: thesis: for F being middle_volume of f,D st f | A is bounded_above holds

middle_sum (f,F) <= upper_sum (f,D)

let F be middle_volume of f,D; :: thesis: ( f | A is bounded_above implies middle_sum (f,F) <= upper_sum (f,D) )

len (upper_volume (f,D)) = len D by INTEGRA1:def 6;

then reconsider p = upper_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_above ; :: thesis: middle_sum (f,F) <= upper_sum (f,D)

for D being Division of A

for F being middle_volume of f,D st f | A is bounded_above holds

middle_sum (f,F) <= upper_sum (f,D)

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_above holds

middle_sum (f,F) <= upper_sum (f,D)

let D be Division of A; :: thesis: for F being middle_volume of f,D st f | A is bounded_above holds

middle_sum (f,F) <= upper_sum (f,D)

let F be middle_volume of f,D; :: thesis: ( f | A is bounded_above implies middle_sum (f,F) <= upper_sum (f,D) )

len (upper_volume (f,D)) = len D by INTEGRA1:def 6;

then reconsider p = upper_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_above ; :: thesis: middle_sum (f,F) <= upper_sum (f,D)

now :: thesis: for i being Nat st i in Seg (len D) holds

q . i <= p . i

hence
middle_sum (f,F) <= upper_sum (f,D)
by RVSUM_1:82; :: thesis: verumq . i <= p . i

let i be Nat; :: thesis: ( i in Seg (len D) implies q . i <= p . i )

assume i in Seg (len D) ; :: thesis: q . i <= p . i

then i in dom D by FINSEQ_1:def 3;

hence q . i <= p . i by A1, Lm4; :: thesis: verum

end;assume i in Seg (len D) ; :: thesis: q . i <= p . i

then i in dom D by FINSEQ_1:def 3;

hence q . i <= p . i by A1, Lm4; :: thesis: verum