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_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let f be Function of A,REAL; for D being Division of A
for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let D be Division of A; for e being Real st f | A is bounded_below & 0 < e holds
ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
let e be Real; ( f | A is bounded_below & 0 < e implies ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e )
len (lower_volume (f,D)) = len D
by INTEGRA1:def 7;
then reconsider p = lower_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_below & 0 < e )
; ex F being middle_volume of f,D st middle_sum (f,F) <= (lower_sum (f,D)) + e
then consider F being middle_volume of f,D such that
A1:
for i being Nat st i in dom D holds
( (lower_volume (f,D)) . i <= F . i & F . i < ((lower_volume (f,D)) . i) + e1 )
by Lm2, XREAL_1:139;
set s = (len D) |-> e1;
reconsider t = p + ((len D) |-> e1) as Element of (len D) -tuples_on REAL ;
take
F
; middle_sum (f,F) <= (lower_sum (f,D)) + e
len F = len D
by Def1;
then reconsider q = F as Element of (len D) -tuples_on REAL by FINSEQ_2:92;
then
Sum q <= Sum t
by RVSUM_1:82;
then
Sum q <= (Sum p) + (Sum ((len D) |-> e1))
by RVSUM_1:89;
then
Sum q <= (Sum p) + ((len D) * e1)
by RVSUM_1:80;
hence
middle_sum (f,F) <= (lower_sum (f,D)) + e
by XCMPLX_1:87; verum