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 ;
A2: C is nonnegative by Def2;
(sigma_Meas C) . A' = C . A' by Def4;
hence 0. <= (sigma_Meas C) . A by A2, MEASURE1:def 4; :: thesis: verum

end;

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

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

end;

C is zeroed by Def2;
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 4, MEASURE1:def 5, VALUED_0:def 19; :: thesis: verum