:: deftheorem defines vol MEASURE7:def 5 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for b₃ being sequence of (Funcs (NAT,ExtREAL)) holds
( b₃ = G vol iff for n being Element of NAT holds b₃ . n = (G . n) vol );