let X be set ; :: thesis: for F being Field_Subset of X

for M being Measure of F holds (C_Meas M) . {} = 0

let F be Field_Subset of X; :: thesis: for M being Measure of F holds (C_Meas M) . {} = 0

let M be Measure of F; :: thesis: (C_Meas M) . {} = 0

(C_Meas M) . {} <= M . {} by Th9, PROB_1:4;

then A1: (C_Meas M) . {} <= 0 by VALUED_0:def 19;

{} X in bool X ;

then {} in dom (C_Meas M) by FUNCT_2:def 1;

then A2: (C_Meas M) . {} in rng (C_Meas M) by FUNCT_1:3;

C_Meas M is nonnegative by Th10;

then rng (C_Meas M) is nonnegative ;

hence (C_Meas M) . {} = 0. by A1, A2; :: thesis: verum

for M being Measure of F holds (C_Meas M) . {} = 0

let F be Field_Subset of X; :: thesis: for M being Measure of F holds (C_Meas M) . {} = 0

let M be Measure of F; :: thesis: (C_Meas M) . {} = 0

(C_Meas M) . {} <= M . {} by Th9, PROB_1:4;

then A1: (C_Meas M) . {} <= 0 by VALUED_0:def 19;

{} X in bool X ;

then {} in dom (C_Meas M) by FUNCT_2:def 1;

then A2: (C_Meas M) . {} in rng (C_Meas M) by FUNCT_1:3;

C_Meas M is nonnegative by Th10;

then rng (C_Meas M) is nonnegative ;

hence (C_Meas M) . {} = 0. by A1, A2; :: thesis: verum