theorem Th36: :: INTEGR19:36

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 D being Division of A
for p being FinSequence of REAL n
for q being FinSequence of (REAL-NS n) st f = g & p = q holds
( p is middle_volume of f,D iff q is middle_volume of g,D )