:: deftheorem Def9 defines induced_Measure MEASURE9:def 8 :
for X being set
for S being semialgebra_of_sets of X
for P being pre-Measure of S
for b₄ being Measure of (Field_generated_by S) holds
( b₄ is induced_Measure of S,P iff for A being set st A in Field_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
b₄ . A = Sum (P * F) );