:: deftheorem Def6 defines integral INTEGR18:def 6 :
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X st f is integrable holds
for b₄ being Point of X holds
( b₄ = integral f iff 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)) = b₄ ) );