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 Th22;
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) ;
consider a, b being R_eal such that
A2: ( a = M . A & b = C . A ) ;
reconsider F' = F as Function of NAT , bool X by FUNCT_2:9;
A3: C * F' is Function of NAT , ExtREAL ;
for k being set st k in NAT holds
(M * F) . k = (C * F) . k

proof

let k be set ; :: thesis: ( k in NAT implies (M * F) . k = (C * F) . k )
assume A4: k in NAT ; :: thesis: (M * F) . k = (C * F) . k
then A5: (M * F) . k = M . (F . k) by FUNCT_2:21;
A6: F . k in sigma_Field C by A4, FUNCT_2:7;
reconsider F = F as Function of NAT , bool X by FUNCT_2:9;
(C * F) . k = C . (F . k) by A4, FUNCT_2:21;
hence (M * F) . k = (C * F) . k by A5, A6, Def4; :: thesis: verum

end;

then A7: M * F = C * F by A3, FUNCT_2:18;
reconsider F = F as Function of NAT , bool X by FUNCT_2:9;
b <= SUM (C * F) by A1, A2, Def2;
hence M . (union (rng F)) <= SUM (M * F) by A1, A2, A7, Def4; :: thesis: verum

end;

hence sigma_Meas C is sigma_Measure of sigma_Field C by MEASURE3:17; :: thesis: verum