:: deftheorem Def5 defines vol MEASURE8:def 5 :
for X being set
for F being Field_Subset of X
for M being Measure of F
for FSets being Set_Sequence of F
for b₅ being ExtREAL_sequence holds
( b₅ = vol (M,FSets) iff for n being Nat holds b₅ . n = M . (FSets . n) );