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
(C_Meas M) . {} = 0. by Th11;
then A1: C_Meas M is zeroed by VALUED_0:def 19;
( C_Meas M is nonnegative & ( for A, B being Subset of X st A c= B holds
( (C_Meas M) . A <= (C_Meas M) . B & ( for F being sequence of (bool X) holds (C_Meas M) . (union (rng F)) <= SUM ((C_Meas M) * F) ) ) ) ) by Th10, Th12, Th13;
hence C_Meas M is C_Measure of X by A1, MEASURE4:def 1; :: thesis: verum