let A be 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:5;
then A3: 1 in dom D1 by FINSEQ_1:def 3;
then A4: lower_bound (divset D1,1) = lower_bound A by Def5;
upper_bound (divset D1,1) = D1 . 1 by A3, Def5
.= upper_bound A by A2, Def2 ;
then divset D1,1 = [.(lower_bound A),(upper_bound A).] by A4, Th5;
then A5: divset D1,1 = A by Th5;
A6: dom f = A by FUNCT_2:def 1;
A7: (lower_volume f,D1) . 1 = (lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by A3, Def8;
len (lower_volume f,D1) = 1 by A2, Def8;
then lower_sum f,D1 = Sum <*((lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)))*> by A7, FINSEQ_1:57
.= (lower_bound (rng (f | A))) * (vol A) by A5, FINSOP_1:12
.= (lower_bound (rng f)) * (vol A) by A6, RELAT_1:97 ;
hence lower_sum f,D1 <= lower_sum f,D2 by A1, Th27; :: thesis: verum