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

let A be Element of sigma_Field C; :: thesis: 0. <= (sigma_Meas C) . A
reconsider A' = A as Subset of X ;
A2: (sigma_Meas C) . A' = C . A' by Def4;
C is nonnegative by Def2;
hence 0. <= (sigma_Meas C) . A by A2, MEASURE1:def 4; :: thesis: verum

end;

X: C is zeroed by Def2;
{} in sigma_Field C by PROB_1:10;
then (sigma_Meas C) . {} = C . {} by Def4;
then A3: ( sigma_Meas C is nonnegative & (sigma_Meas C) . {} = 0. ) by A1, X, MEASURE1:def 4, VALUED_0:def 19;

now

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) )
assume A4: A misses B ; :: thesis: (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B)
reconsider A' = A, B' = B as Subset of X ;
A5: ( (sigma_Meas C) . A' = C . A' & (sigma_Meas C) . B' = C . B' ) by Def4;
C . (A' \/ B') = (C . A') + (C . B') by A4, Th15;
hence (sigma_Meas C) . (A \/ B) = ((sigma_Meas C) . A) + ((sigma_Meas C) . B) by A5, Def4; :: thesis: verum

end;

hence sigma_Meas C is Measure of (sigma_Field C) by A3, MEASURE1:def 5, VALUED_0:def 19; :: thesis: verum