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 g being Function of A,(REAL-NS n)
for T being DivSequence of A
for p being sequence of ((REAL n) *)
for q being sequence of ( the carrier of (REAL-NS n) *) st f = g & p = q holds
( p is middle_volume_Sequence of f,T iff q is middle_volume_Sequence of g,T )