let X be set ; :: thesis: for C being C_Measure of X holds sigma_Meas C is Measure of (sigma_Field C)
let C be C_Measure of X; :: thesis: sigma_Meas C is Measure of (sigma_Field C)

A1: now :: thesis: for A being Element of sigma_Field C holds 0. <= (sigma_Meas C) . A

let A be Element of sigma_Field C; :: thesis: 0. <= (sigma_Meas C) . A
reconsider A9 = A as Subset of X ;
A2: C is nonnegative by Def1;
(sigma_Meas C) . A9 = C . A9 by Def3;
hence 0. <= (sigma_Meas C) . A by A2, MEASURE1:def 2; :: thesis: verum

end;

{} in sigma_Field C by PROB_1:4;
then A3: (sigma_Meas C) . {} = C . {} by Def3;

A4: now :: thesis: for A, B being Element of sigma_Field C st A misses B holds
(sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B)

let A, B be Element of sigma_Field C; :: thesis: ( A misses B implies (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) )
reconsider A9 = A, B9 = B as Subset of X ;
A5: (sigma_Meas C) . B9 = C . B9 by Def3;
assume A misses B ; :: thesis: (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B)
then A6: C . (A9 \/ B9) = (C . A9) + (C . B9) by Th6;
(sigma_Meas C) . A9 = C . A9 by Def3;
hence (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) by A5, A6, Def3; :: thesis: verum

end;

C is zeroed by Def1;
then (sigma_Meas C) . {} = 0. by A3, VALUED_0:def 19;
hence sigma_Meas C is Measure of (sigma_Field C) by A1, A4, MEASURE1:def 2, MEASURE1:def 8, VALUED_0:def 19; :: thesis: verum