for X being RealBanachSpace
for A being non empty closed_interval Subset of REAL
for h being Function of A, the carrier of X st ( for r being Real st 0 < r holds
ex s being Real st
( 0 < s & ( for x1, x2 being Real st x1 in dom h & x2 in dom h & |.(x1 - x2).| < s holds
||.((h /. x1) - (h /. x2)).|| < r ) ) ) holds
for T being DivSequence of A
for S being middle_volume_Sequence of h,T st delta T is convergent & lim (delta T) = 0 holds
middle_sum (h,S) is convergent