let A be non empty closed_interval Subset of REAL; 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; 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; 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; ( 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 )
; ( 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; verum