theorem Th11: :: INTEGR15:11

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

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 )

for A being non empty closed_interval Subset of REAL

for f being Function of A,(REAL n)

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 )