:: deftheorem Def10 defines On MEASURE8:def 10 :
for X being set
for F being Field_Subset of X
for Sets being SetSequence of X
for Cvr being Covering of Sets,F
for b₅ being Covering of union (rng Sets),F holds
( b₅ = On Cvr iff for n being Nat holds b₅ . n = (Cvr . ((pr1 InvPairFunc) . n)) . ((pr2 InvPairFunc) . n) );