let A be non empty 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 )
f | A is bounded_below by A1;
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 ;
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;
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