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 that
A1: f is bounded and
A2: f is integrable and
A3: ( delta T is convergent & lim (delta T) = 0 ) ; :: thesis: ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f )
A4: dom f = A by FUNCT_2:def 1;
then f | A is bounded_below by A1, RELAT_1:98;
then A5: for i being Element of NAT holds (lower_sum f,T) . i <= (middle_sum f,S) . i by Th5;
A6: f | A = f by A4, RELAT_1:98;
then A7: ( lower_sum f,T is convergent & upper_sum f,T is convergent ) by A1, A3, INTEGRA4:8, INTEGRA4:9;
f | A is bounded_above by A1, A4, RELAT_1:98;
then A8: for i being Element of NAT holds (middle_sum f,S) . i <= (upper_sum f,T) . i by Th6;
A9: (lim (upper_sum f,T)) - (lim (lower_sum f,T)) = 0 by A1, A2, A3, A6, INTEGRA4:12;
then lim (lower_sum f,T) = integral f by A1, A3, A6, INTEGRA4:9;
hence ( middle_sum f,S is convergent & lim (middle_sum f,S) = integral f ) by A7, A9, A5, A8, Lm5; :: thesis: verum