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_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:3;
then A3: 1 in dom D1 by FINSEQ_1:def 3;
then A4: lower_bound (divset (D1,1)) = lower_bound A by Def3;
A5: divset (D1,1) = [.(lower_bound (divset (D1,1))),(upper_bound (divset (D1,1))).] by Th2;
upper_bound (divset (D1,1)) = D1 . 1 by A3, Def3
.= upper_bound A by A2, Def1 ;
then A6: divset (D1,1) = A by A4, A5, Th2;
A7: (upper_volume (f,D1)) . 1 = (upper_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) by A3, Def5;
reconsider ubv = (upper_bound (rng (f | (divset (D1,1))))) * (vol (divset (D1,1))) as Element of REAL by XREAL_0:def 1;
len (upper_volume (f,D1)) = 1 by A2, Def5;
then upper_sum (f,D1) = Sum <*ubv*> by A7, FINSEQ_1:40
.= (upper_bound (rng (f | A))) * (vol A) by A6, FINSOP_1:11
.= (upper_bound (rng f)) * (vol A) ;
hence upper_sum (f,D1) >= upper_sum (f,D2) by A1, Th25; :: thesis: verum