:: deftheorem Def3 defines middle_volume_Sequence INTEGR22:def 6 :
for A being non empty closed_interval Subset of REAL
for rho being Function of A,REAL
for u being PartFunc of REAL,REAL
for T being DivSequence of A
for b₅ being sequence of (REAL *) holds
( b₅ is middle_volume_Sequence of rho,u,T iff for k being Element of NAT holds b₅ . k is middle_volume of rho,u,T . k );