:: 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_{5} being sequence of ((REAL n) *) holds

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

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

( b