let A be non empty closed_interval Subset of REAL; for f being Function of A,REAL
for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let f be Function of A,REAL; for D being Division of A
for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let D be Division of A; for e being Real st f | A is bounded_above & 0 < e holds
ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
let e be Real; ( f | A is bounded_above & 0 < e implies ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F) )
len (upper_volume (f,D)) = len D
by INTEGRA1:def 6;
then reconsider p = upper_volume (f,D) as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
reconsider e1 = e / (len D) as Element of REAL by XREAL_0:def 1;
assume
( f | A is bounded_above & 0 < e )
; ex F being middle_volume of f,D st (upper_sum (f,D)) - e <= middle_sum (f,F)
then consider F being middle_volume of f,D such that
A1:
for i being Nat st i in dom D holds
( F . i <= (upper_volume (f,D)) . i & ((upper_volume (f,D)) . i) - e1 < F . i )
by Lm3, XREAL_1:139;
set s = (len D) |-> e1;
reconsider t = p - ((len D) |-> e1) as Element of (len D) -tuples_on REAL ;
take
F
; (upper_sum (f,D)) - e <= middle_sum (f,F)
len F = len D
by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
then
Sum t <= Sum q
by RVSUM_1:82;
then
(Sum p) - (Sum ((len D) |-> e1)) <= Sum q
by RVSUM_1:90;
then
(Sum p) - ((len D) * e1) <= Sum q
by RVSUM_1:80;
hence
(upper_sum (f,D)) - e <= middle_sum (f,F)
by XCMPLX_1:87; verum