let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X
for P being pre-Measure of S ex M being Function of (Ring_generated_by S),ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: for P being pre-Measure of S ex M being Function of (Ring_generated_by S),ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )
let P be pre-Measure of S; :: thesis: ex M being Function of (Ring_generated_by S),ExtREAL st
( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )
consider M being zeroed V224() additive Function of (Ring_generated_by S),ExtREAL such that
A1: for A being set st A in Ring_generated_by S holds
for F being disjoint_valued FinSequence of S st A = Union F holds
M . A = Sum (P * F) by Th46;
take M ; :: thesis: ( M . {} = 0 & ( for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) ) )
thus M . {} = 0 by VALUED_0:def 19; :: thesis: for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K)
thus for K being disjoint_valued FinSequence of S st Union K in Ring_generated_by S holds
M . (Union K) = Sum (P * K) by A1; :: thesis: verum