theorem Th10: :: INTEGR15:10

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL st f is bounded holds

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )

for f being Function of A,REAL st f is bounded holds

( f is integrable iff ex I being Real st

for T being DivSequence of A

for S being middle_volume_Sequence of f,T st delta T is convergent & lim (delta T) = 0 holds

( middle_sum (f,S) is convergent & lim (middle_sum (f,S)) = I ) )