let X be set ; :: thesis: for S being semialgebra_of_sets of X
for P being pre-Measure of S
for M being induced_Measure of S,P holds M is completely-additive
let S be semialgebra_of_sets of X; :: thesis: for P being pre-Measure of S
for M being induced_Measure of S,P holds M is completely-additive
let P be pre-Measure of S; :: thesis: for M being induced_Measure of S,P holds M is completely-additive
let M be induced_Measure of S,P; :: thesis: M is completely-additive
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
M . A = Sum (P * F) by Def9;
hence M is completely-additive by Th59; :: thesis: verum