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 f | A is bounded_below & len D1 = 1 holds
lower_sum (f,D1) <= lower_sum (f,D2)
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded_below & len D1 = 1 holds
lower_sum (f,D1) <= lower_sum (f,D2)
let f be Function of A,REAL; :: thesis: ( f | A is bounded_below & len D1 = 1 implies lower_sum (f,D1) <= lower_sum (f,D2) )
assume that
A1: f | A is bounded_below and
A2: len D1 = 1 ; :: thesis: lower_sum (f,D1) <= lower_sum (f,D2)
1 in Seg (len D1) by A2, FINSEQ_1:3;
then A3: 1 in dom D1 by FINSEQ_1:def 3;
then A4: lower_bound (divset (D1,1)) = lower_bound A by Def3;
upper_bound (divset (D1,1)) = D1 . 1 by A3, Def3
.= upper_bound A by A2, Def1 ;
then divset (D1,1) = [.(lower_bound A),(upper_bound A).] by A4, Th2;
then A5: divset (D1,1) = A by Th2;
A6: (lower_volume (f,D1)) . 1 = (lower_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) by A3, Def6;
reconsider lbv = (lower_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) as Element of REAL by XREAL_0:def 1;
len (lower_volume (f,D1)) = 1 by A2, Def6;
then lower_sum (f,D1) = Sum <*lbv*> by A6, FINSEQ_1:40
.= (lower_bound (rng (f | A))) * (vol A) by A5, FINSOP_1:11
.= (lower_bound (rng f)) * (vol A) ;
hence lower_sum (f,D1) <= lower_sum (f,D2) by A1, Th23; :: thesis: verum