:: deftheorem Def3 defines middle_volume_Sequence INTEGR18:def 3 :
for X being RealNormSpace
for A being non empty closed_interval Subset of REAL
for f being Function of A, the carrier of X
for T being DivSequence of A
for b₅ being sequence of ( the carrier of X *) 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 );