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_above & len D1 = 1 holds
upper_sum f,D1 >= upper_sum f,D2
let D1, D2 be Division of A; :: thesis: for f being Function of A,REAL st f | A is bounded_above & len D1 = 1 holds
upper_sum f,D1 >= upper_sum f,D2
let f be Function of A,REAL ; :: thesis: ( f | A is bounded_above & len D1 = 1 implies upper_sum f,D1 >= upper_sum f,D2 )
assume that
A1: f | A is bounded_above and
A2: len D1 = 1 ; :: thesis: upper_sum f,D1 >= upper_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;
A5: divset D1,1 = [.(lower_bound (divset D1,1)),(upper_bound (divset D1,1)).] by Th5;
upper_bound (divset D1,1) = D1 . 1 by A3, Def5
.= upper_bound A by A2, Def2 ;
then A6: divset D1,1 = A by A4, A5, Th5;
A7: dom f = A by FUNCT_2:def 1;
A8: (upper_volume f,D1) . 1 = (upper_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)) by A3, Def7;
len (upper_volume f,D1) = 1 by A2, Def7;
then upper_sum f,D1 = Sum <*((upper_bound (rng (f | (divset D1,1)))) * (vol (divset D1,1)))*> by A8, FINSEQ_1:57
.= (upper_bound (rng (f | A))) * (vol A) by A6, FINSOP_1:12
.= (upper_bound (rng f)) * (vol A) by A7, RELAT_1:97 ;
hence upper_sum f,D1 >= upper_sum f,D2 by A1, Th29; :: thesis: verum