let A be closed-interval Subset of REAL ; :: thesis: for D1, D2 being Division of A
for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds
upper_sum f,D2 <= upper_sum f,D1
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st D1 <= D2 & f | A is bounded_above holds
upper_sum f,D2 <= upper_sum f,D1
let f be Function of A,REAL ; :: thesis: ( D1 <= D2 & f | A is bounded_above implies upper_sum f,D2 <= upper_sum f,D1 )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_above ; :: thesis: upper_sum f,D2 <= upper_sum f,D1
len D1 in Seg (len D1) by FINSEQ_1:5;
then len D1 in dom D1 by FINSEQ_1:def 3;
then (PartSums (upper_volume f,D1)) . (len D1) >= (PartSums (upper_volume f,D2)) . (indx D2,D1,(len D1)) by A1, A2, Th42;
then upper_sum f,D1 >= (PartSums (upper_volume f,D2)) . (indx D2,D1,(len D1)) by Th44;
then upper_sum f,D1 >= (PartSums (upper_volume f,D2)) . (len D2) by A1, Th46;
hence upper_sum f,D2 <= upper_sum f,D1 by Th44; :: thesis: verum