:: deftheorem Def3 defines middle_volume_Sequence INTEGR15:def 3 :

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for b_{4} being sequence of (REAL *) holds

( b_{4} is middle_volume_Sequence of f,T iff for k being Element of NAT holds b_{4} . k is middle_volume of f,T . k );

for A being non empty closed_interval Subset of REAL

for f being Function of A,REAL

for T being DivSequence of A

for b

( b