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_below holds
lower_sum (f,D2) >= lower_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_below holds
lower_sum (f,D2) >= lower_sum (f,D1)
let f be Function of A,REAL; :: thesis: ( D1 <= D2 & f | A is bounded_below implies lower_sum (f,D2) >= lower_sum (f,D1) )
assume that
A1: D1 <= D2 and
A2: f | A is bounded_below ; :: thesis: lower_sum (f,D2) >= lower_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 (lower_volume (f,D1))) . (len D1) <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,(len D1))) by A1, A2, Th39;
then lower_sum (f,D1) <= (PartSums (lower_volume (f,D2))) . (indx (D2,D1,(len D1))) by Th41;
then lower_sum (f,D1) <= (PartSums (lower_volume (f,D2))) . (len D2) by A1, Th42;
hence lower_sum (f,D2) >= lower_sum (f,D1) by Th41; :: thesis: verum