:: deftheorem Def7 defines middle_volume_Sequence INTEGR15:def 7 :
for n being Element of NAT
for A being non empty closed_interval Subset of REAL
for f being Function of A,(REAL n)
for T being DivSequence of A
for b₅ being sequence of ((REAL n) *) holds
( b₅ is middle_volume_Sequence of f,T iff for k being Element of NAT holds b₅ . k is middle_volume of f,T . k );