let X be set ; :: thesis: for C being C_Measure of X holds sigma_Meas C is sigma_Measure of (sigma_Field C)
let C be C_Measure of X; :: thesis: sigma_Meas C is sigma_Measure of (sigma_Field C)
reconsider M = sigma_Meas C as Measure of (sigma_Field C) by Th13;
for F being Sep_Sequence of (sigma_Field C) holds M . (union (rng F)) <= SUM (M * F)

proof

let F be Sep_Sequence of (sigma_Field C); :: thesis: M . (union (rng F)) <= SUM (M * F)
consider A being Subset of X such that
A1: A = union (rng F) ;
A2: for k being object st k in NAT holds
(M * F) . k = (C * F) . k

proof

let k be object ; :: thesis: ( k in NAT implies (M * F) . k = (C * F) . k )
assume A3: k in NAT ; :: thesis: (M * F) . k = (C * F) . k
then A4: (M * F) . k = M . (F . k) by FUNCT_2:15;
A5: F . k in sigma_Field C by A3, FUNCT_2:5;
reconsider F = F as sequence of (bool X) by FUNCT_2:7;
(C * F) . k = C . (F . k) by A3, FUNCT_2:15;
hence (M * F) . k = (C * F) . k by A4, A5, Def3; :: thesis: verum

end;

reconsider F9 = F as sequence of (bool X) by FUNCT_2:7;
consider a, b being R_eal such that
a = M . A and
A6: b = C . A ;
C * F9 is sequence of ExtREAL ;
then A7: M * F = C * F by A2, FUNCT_2:12;
reconsider F = F as sequence of (bool X) by FUNCT_2:7;
b <= SUM (C * F) by A1, A6, Def1;
hence M . (union (rng F)) <= SUM (M * F) by A1, A6, A7, Def3; :: thesis: verum

end;

hence sigma_Meas C is sigma_Measure of (sigma_Field C) by MEASURE3:14; :: thesis: verum