for A being non empty closed_interval Subset of REAL
for D being Division of A
for rho being Function of A,REAL
for B being non empty closed_interval Subset of REAL
for v being FinSequence of REAL st B c= A & len D = len v & ( for i being Nat st i in dom v holds
v . i = vol ((B /\ (divset (D,i))),rho) ) holds
Sum v = vol (B,rho)