let A be 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 )
assume AS: f | A is bounded_above ; :: thesis: middle_sum f,F <= upper_sum f,D
A1: len (upper_volume f,D) = len D by INTEGRA1:def 7;
B1: len F = len D by defx0;
reconsider p = upper_volume f,D as Element of (len D) -tuples_on REAL by A1, FINSEQ_2:110;
reconsider q = F as Element of (len D) -tuples_on REAL by B1, FINSEQ_2:110;

now

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 AS, PX0102; :: thesis: verum

end;

hence middle_sum f,F <= upper_sum f,D by RVSUM_1:112; :: thesis: verum