let X be set ; :: thesis: for F being Field_Subset of X
for M being Measure of F holds C_Meas M is C_Measure of X
let F be Field_Subset of X; :: thesis: for M being Measure of F holds C_Meas M is C_Measure of X
let M be Measure of F; :: thesis: C_Meas M is C_Measure of X
P1: C_Meas M is nonnegative by M8Th6;
(C_Meas M) . {} = 0. by M8Th7;
then P2: C_Meas M is zeroed by VALUED_0:def 19;
for A, B being Subset of X st A c= B holds
( (C_Meas M) . A <= (C_Meas M) . B & ( for F being Function of NAT ,(bool X) holds (C_Meas M) . (union (rng F)) <= SUM ((C_Meas M) * F) ) ) by M8Th8, M8Th9;
hence C_Meas M is C_Measure of X by P1, P2, MEASURE4:def 2; :: thesis: verum