theorem :: INTEGR15:12

for n being Element of NAT

for A being non empty closed_interval Subset of REAL

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

( f is integrable iff ex I being Element of REAL n 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 A being non empty closed_interval Subset of REAL

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

( f is integrable iff ex I being Element of REAL n 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 ) )