:: deftheorem Def4 defines tagged_volume COUSIN2:def 8 :
for I being non empty closed_interval Subset of REAL
for f being PartFunc of I,REAL
for TD being tagged_division of I
for b₄ being FinSequence of REAL holds
( b₄ = tagged_volume (f,TD) iff ( len b₄ = len TD & ( for i being Nat st i in dom TD holds
b₄ . i = (f . ((tagged_of TD) . i)) * (vol (divset ((division_of TD),i))) ) ) );