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

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