:: deftheorem Def11 defines On MEASURE7:def 11 :
for F being sequence of (bool REAL)
for G being Interval_Covering of F
for H being sequence of [:NAT,NAT:] st rng H = [:NAT,NAT:] holds
for b₄ being Interval_Covering of union (rng F) holds
( b₄ = On (G,H) iff for n being Element of NAT holds b₄ . n = (G . ((pr1 H) . n)) . ((pr2 H) . n) );