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 A4: 1 in dom D1 by FINSEQ_1:def 3;
A5: divset D1,1 = A

proof

A6: lower_bound (divset D1,1) = lower_bound A by A4, Def5;
upper_bound (divset D1,1) = D1 . 1 by A4, Def5
.= upper_bound A by A2, Def2 ;
then divset D1,1 = [.(lower_bound A),(upper_bound A).] by A6, Th5;
hence divset D1,1 = A by Th5; :: thesis: verum

end;

A7: dom f = A by FUNCT_2:def 1;
A8: len (lower_volume f,D1) = 1 by A2, Def8;
(lower_volume f,D1) . 1 = (lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by Def8, A4;
then lower_sum f,D1 = Sum <*((lower_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)))*> by A8, FINSEQ_1:57
.= (lower_bound (rng (f | A))) * (vol A) by A5, FINSOP_1:12
.= (lower_bound (rng f)) * (vol A) by A7, RELAT_1:97 ;
hence lower_sum f,D1 <= lower_sum f,D2 by A1, Th27; :: thesis: verum