let A be closed-interval Subset of REAL ; :: thesis: for f being Function of A,REAL
for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let f be Function of A,REAL ; :: thesis: for T being DivSequence of A
for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let T be DivSequence of A; :: thesis: for S being middle_volume_Sequence of f,T st f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 holds
( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
let S be middle_volume_Sequence of f,T; :: thesis: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 implies ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f ) )
assume AS1: ( f is bounded & f is integrable & delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
X0: dom f = A by FUNCT_2:def 1;
then X1: f | A = f by RELAT_1:98;
Q1: f | A is bounded_below by X0, RELAT_1:98, AS1;
Q2: f | A is bounded_above by X0, RELAT_1:98, AS1;
P1: lower_sum f,T is convergent by INTEGRA4:8, AS1, X1;
P2: upper_sum f,T is convergent by INTEGRA4:9, AS1, X1;
P3: (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by INTEGRA4:12, AS1, X1;
then P4: lim (lower_sum f,T) = integral f by X1, INTEGRA4:9, AS1;
P5: for i being Element of NAT holds (lower_sum f,T) . i <= (middle_sum f,S) . i by Q1, PX011;
for i being Element of NAT holds (middle_sum f,S) . i <= (upper_sum f,T) . i by Q2, PX012;
hence ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f ) by P1, P2, P3, P4, P5, PX041; :: thesis: verum