let A be non empty 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:3;
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, Th38;
then upper_sum (f,D1) >= (PartSums (upper_volume (f,D2))) . (indx (D2,D1,(len D1))) by Th40;
then upper_sum (f,D1) >= (PartSums (upper_volume (f,D2))) . (len D2) by A1, Th42;
hence upper_sum (f,D2) <= upper_sum (f,D1) by Th40; :: thesis: verum