:: deftheorem Def6 defines lower_volume INTEGRA1:def 7 :
for A being non empty closed_interval Subset of REAL
for f being PartFunc of A,REAL
for D being Division of A
for b₄ being FinSequence of REAL holds
( b₄ = lower_volume (f,D) iff ( len b₄ = len D & ( for i being Nat st i in dom D holds
b₄ . i = (lower_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) ) );