theorem Th6: :: INTEGR20:6

for A being non empty closed_interval Subset of REAL
for D being Division of A
for q being FinSequence of REAL st dom q = Seg (len D) & ( for i being Nat st i in Seg (len D) holds
q . i = vol (divset (D,i)) ) holds
Sum q = vol A