for A being non empty closed_interval Subset of REAL
for D being Division of A
for f being Function of A,REAL holds (PartSums (lower_volume (f,D))) . (len D) = lower_sum (f,D)