:: deftheorem Def5 defines upper_volume INTEGRA1:def 6 :
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₄ = upper_volume (f,D) iff ( len b₄ = len D & ( for i being Nat st i in dom D holds
b₄ . i = (upper_bound (rng (f | (divset (D,i))))) * (vol (divset (D,i))) ) ) );