:: deftheorem Def3 defines middle_volume_Sequence INTEGR16:def 3 :
for A being non empty closed_interval Subset of REAL
for f being Function of A,COMPLEX
for T being DivSequence of A
for b₄ being sequence of (COMPLEX *) 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 );